§P415 Homework Assignment

Instructions:

• Using PVS, prove the theorems in N.pvs.

Notes and Hints:

• These hints will be discussed thoroughly in class, but it is worthwhile to read about them in the Prover Manual and spend some time exploring them beforehand.

• None of the theorems in this file are proved with induct

• This file contains four theories looking at issues surrounding data-type modeling, and representation verification, as discussed in class. The formulations include new syntax for

  • record declarations [# ... #] and constructions (# ... #)

  • array declarations ARRAY [index -> content] and construction LAMBDA expressions.

  • updating (or "extending") using WITH

• In fact, arrays and records are both "syntactic sugar" for (represented as) functions in the PVS logic. The primary reasoning rules for functions are:

  • (extensionality type) and (apply-extensionality formula), which have to do with function equality

  • beta, which is analgous to expand.

  • I don't think beta, is needed for this assignment.

• In most (LAMDA arg : body) expressions, the body is a conditional expression, so lift-if and case, are heavily used.

• lift-if also works on WITH and CASES expressions.