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*.