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?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
1
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.
answered Nov 17, 2016 at 15:02
-
$\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$ Commented Nov 17, 2016 at 21:34