0
$\begingroup$

Say I have a function like this:

function colorize(integer) {
  var hex = '#'

  if (integer > 1) hex += 'ff'
  else hex += '00'
  if (integer < 100) hex += 'aa'
  else hex += 'bb'
  if (integer > 10) hex += '11'
  else hex += '22'

  return hex
}

It returns CSS hex colors, not named colors or rgb(...) values or anything else. For now we can ignore the low-level / platform specific details of JavaScript and hardware and just deal with this abstractly as if it was in a perfect environment.

The goal is to use small step operational semantics to prove that it returns a CSS hex color. If it requires too much initialization to do the proof, then assume the initialization is already handled so all that's focused on is the specific function and its implementation.

From my understanding this means we would have some rule for var, =, if, ===, +=, and return. In addition, there is sort of a trace, since it is modifying the value in memory step by step.

From my understanding this would involve using the operational semantics configuration evaluation〈a, σ〉→〈a', σ'〉like:

〈=, σ〉→〈=, σ'[hex ↦ #]〉
   →
〈if (e) x else y, σ〉→〈...〉
   →
   ...

I am not sure how to:

  1. Actually write the configurations out.
  2. Write out the sequence of the evaluations.
  3. Write a proof that the output will be a hex string such as #00aa22 if given 0 for example.

I was wondering if one could point me in the right direction on how to solve this. Basically:

  1. What some configurations look like using this function as an example.
  2. What a sequence of the evaluations (or trace) looks like.
  3. What a proof would entail (not the actual proof as I imagine there will be lots of steps), maybe just the first few steps of the proof.

Thank you very much for your help.

$\endgroup$
  • $\begingroup$ Using the operational semantics directly can be tedious and error-prone. Especially small-step semantics. Axiomatic semantics (Hoare logic or separation logic) usually makes it easier to prove results, which, by a correctness theorem, do hold also according to the operational semantics. $\endgroup$ – chi May 28 '18 at 13:36
  • $\begingroup$ @chi would be interested to know why/how operational semantics is error prone. $\endgroup$ – Lance Pollard May 28 '18 at 19:08
  • $\begingroup$ To prove a property involving small step semantics one has to find a single invariant which is true at every small step of computation, for the whole program. To do the same thing using axiomatic semantics, one has to find an invariant for each loop (which does not have to be true in the middle of the iteration). Loops usually are smaller than the whole program, and the loop invariants usually are much smaller than whole-program, small-step invariants. For your short program, probably both approaches can be used effectively, but Hoare logic should be simpler to use. $\endgroup$ – chi May 28 '18 at 19:55
2
$\begingroup$

You are looking for Hoare logic. Writing out the answer to the question would pretty much amount to copying the introduction to Hoare logic from Wikipedia. I suggest that you have a look at proving program correctness using Hoare logic, and try to apply it to your problem. It's actually an easy case because there are no loops. If you get stuck, come back and ask a specific question about Hoare logic.

I would break up the problem into proving several properties about hex:

  1. The length of hex is 7 at the end.
  2. The first character of hex is #.
  3. All characters, except the first one, are hexadecimal digits.

Also not that the proof does not require you to write out any operational semantics. You can just use the Hoare logic to argue about your program, and there is a theorem which guarantees that Hoare logic is correct with respect to the standard operational semantics.

$\endgroup$
  • $\begingroup$ I was going to try Hoare Logic, but this presentation on Matching Logic Reachability made it sound bad. "Not easy to define and understand, error-prone. Not executable, hard to test; require program transformations which may lose behaviors, etc." Said state of the art is operational semantics. $\endgroup$ – Lance Pollard May 28 '18 at 19:04
  • $\begingroup$ For the easy program that you are considering those criticisms do not apply, and in any case there are extensions of Hoare logic that work quite well. $\endgroup$ – Andrej Bauer May 28 '18 at 19:15
  • $\begingroup$ If you're interested in doing this for real, have a look at a state-of-the-art tool such as ynot. $\endgroup$ – Andrej Bauer May 28 '18 at 19:20
  • $\begingroup$ Yes I am interested in doing this for real, this was just a simplified example to get started. $\endgroup$ – Lance Pollard May 28 '18 at 19:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.