I'm studying program verification and came across the following triple:
$$ \{\top\} \;P \; \{y=(x+1)\} $$ What's the meaning of the $\top$ symbol on the precondition? Does it mean $P$ can take any input?


The symbol $\top$, known as top, stands for "True". There is also a symbol $\bot$, known as bottom, which stands for "False". Top is always true, and bottom is always false. In your case, having a precondition that always holds is the same as having no precondition.

  • $\begingroup$ To be pedantic, I will point out that the meaning of "top" and "bottom" depends on the specific logical system - and maybe some other contexts ;) $\endgroup$ – gardenhead Nov 17 '16 at 21:34

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.