verus
forked from verus-lang/verus
Star 0
Fork 0
Watch
verus source docs guide src reference-specification-language.md
290 B · 7 lines
Markdown
at master

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.