fileec / dafnysos Goto Github PK
View Code? Open in Web Editor NEWUsing the Dafny verification language to specify the design of a toy imperative language (WHILE-like). The design includes the syntax, small step operational semantics, type system and proof system of the language. Consequently, we can enjoy the verification capability of Dafny to prove theorem/lemma such as type soundness by stepping, the soundness of proof system.