Summary: A list of Spec# specific keywords (alphabetical).
Nearby: FrequentlyAskedQuestions


Many of these keywords are context dependent. That is, they may be used as ordinary identifiers outside of certain contexts. For each keyword, we will try to indicate whether it is context dependent or not.

acquire

additive

assert

Used as a statement in a method: assert E; where E is a boolean expression. At runtime, it throws an exception if the expression evaluates to false, otherwise it is a nop. For static verification, Boogie will issue an error if it cannot validate (prove) the condition at that program point.

assume

Used as a statement in a method: assume E; where E is a boolean expression. At runtime, it acts just as the assert statement: it throws an exception if the expression evaluates to false, otherwise it is a nop. For static verification, it adds the expression to the list of facts that the theorem prover has available to discharge proof obligations with. You should use assume when there is something that cannot be handled by the theorem prover, but which you feel can absolutely be depended on. (Or if you just want to silence that particular error message from Boogie.)

at

count

elements_seen

ensures

exists

expose

forall

invariant

modifies

old

otherwise

read

requires

throws