Specification language
Here we formally describe Verus’s specification language, which is used for
assert, requires, ensures, and so on.
We start with the semantics
of its types and then the syntax and semantics of its
expressions.
Press ← or → to navigate between chapters
Press S or / to search in the book
Press ? to show this help
Press Esc to hide this help
Here we formally describe Verus’s specification language, which is used for
assert, requires, ensures, and so on.
We start with the semantics
of its types and then the syntax and semantics of its
expressions.