CSCI P415/515 Fri Jan 6 15:18:04 EST 2012 [SDJ]

Homework Assignment


  1. Copy PVS source file N.pvs into your working directory.
  2. Prove all the theorems.
  3. Turn in all source (.pvs), proof (.prf) and status (.status) files.

Notes and Hints:

This assignment illustrates specification and implementation of non-inductive Abstract Data Type and issues arise in the underlying mathematics.