What's the meaning of the example statement here?

"A service specification S describes an interface: it specifies the behavior of certain program elements (functions or subprograms) through statements expressed in program logic. For instance, these might be such statements:

  1. [...]
  2. x, y : N[{x>0} y := x * x {y > x}]


The quote is from the article "On The Hourglass Model" By Micah Beck, Communications of the ACM, July 2019, Vol. 62 No. 7, Pages 48-57


That means:

    For all natural numbers x and y,
      if the value of variable x is greater than zero
      then after the assignment statement "y := x*x" is executed
      the predicate "y > x" will be true.

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.