Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?

“Here’s an example. In one integer variable x , the specification x′=x ∨ x′=x+1 says that the final value of x is either the same as the initial value or one greater. Let’s compose it with itself.

   x′=x ∨ x′=x+1 . x′=x ∨ x′=x+1
= ∃x′′· (x′′=x ∨ x′′=x+1) ∧ (x′=x′′ ∨ x′=x′′+1) 
 distribute ∧ over ∨
= ∃x′′· x′′=x ∧ x′=x′′ ∨ x′′=x+1 ∧ x′=x′′ ∨ x′′=x ∧ x′=x′′+1 ∨ x′′=x+1 ∧ x′=x′′+1   
 distribute ∃ over ∨
= (∃x′′· x′′=x ∧ x′=x′′) ∨ (∃x′′· x′′=x+1 ∧ x′=x′′) ∨ (∃x′′· x′′=x ∧ x′=x′′+1) ∨ (∃x′′· x′′=x+1 ∧ x′=x′′+1) 
 One Point, 4 times
= x′=x ∨ x′=x+1 ∨ x′=x+2

“If we either leave x alone or add 1 to it, and then again we either leave x alone or add 1 to it, the net result is that we either leave it alone, add 1 to it, or add 2 to it.”

– Eric Hehner, http://www.cs.toronto.edu/~hehner/aPToP/ page 37

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment