CSCI P545 Sat Jan 24 11:14:37 EST 2009 © [SDJ]

Homework Assignment

Instructions:

Do part 1 and either 2 (recommended) or 3, (but look at both).
  1. Copy PVS source files N.pvs and into your working directory.

    Prove all theorems in N.pvs

  2. The file M.tgz is a compressed tar archive of a directory. Place a copy of that directory in your working area and expand it. You will find a directory, M, that contains:

    Prove all the theorems (and try the TCCs).

  3. The file S.tgz is a compressed tar archive of a directory. Place a copy of that directory in your working area and expand it. You should find a directory S containing containing PVS files S/S.pvs [PVS] and S/S.pfr [PRF]

    Prove all the theorems.

Notes and Hints:

  1. N.pvs Introduces the PVS array and record constructs. You can read more about them in the PVS Language Reference [PDF]. Pay particular attention to with clauses.

    Arrays and records are represented by functions in the PVS logic. The rule for proving function equality is based on the Principle of Extensionality, which says, ``Two functions, f and g are provably equal if they give equal results for all possible arguments.'' That is,

    f = g  if  ∀x: f(x) = g(x)
    The Prover command (apply-extensionality n) instantiates this principle, if applicable, for sequent formula n.
  2. Directory M contains a tutorial for a list search project, including a report [PDF], that illustrates the organization and content I am looking for in project reports. This material will be discussed further in lecture. The actual project would be based on a different data structure.
  3. Directory S contains a similar tutorial for the sorting project, but does not include a sample report. So if you decide to work on this part, you should still review the material in directory M. The actual project would involve more sophisticated algorithms.