CAS 707 ─ Formal Specification Techniques ─ Winter 2018
Assignment 3
Please submit PDF, LaTeX source, and F* source to subversion as usual.
Assignment 3.1: evalExpr
Complete the expression evaluation function we started in class. Revise design decisions as necessary, respectively as you feel appropriate, and document your motivations and experiences.
Assignment 3.2: showsExpr
Write a showS
function showsExpr
for our expression datatype.
Take care to insert parentheses at least as far as needed for unambiguous parsing.
Strive to insert not more parentheses than necessary.
(For example, take the approach of the Haskell type class Show
and implement showsPrecExpr : #t:ty -> nat -> expr t -> showS
,
where the nat
argument is the precedence of the context of the
current call.)
Assignment 3.3: execStmt
Write a function execStmt
that implements statement execution
as state transformation.
Assignment 3.4: Introduction to Hoare logic
- Read the Wikipedia page on Hoare logic.
- Start familiarising yourself with Chapter 5 of RSD. Recognise the expression and statement (“command”) types they are using there as closely related to the ones we are using, and explore implementing additional material in F*.