Note: Make sure that you allocate enough time to the project. As a rough guideline, I suggest that you complete parts 1 and 2 below by September 25.
:trans1
(defun-g set-union (X Y)
"set union, i.e., X U Y"
(declare (xargs :guard (true-listp X)))
((implies (true-listp Y) (true-listp (set-union X Y)))
:rule-classes :type-prescription)
(if (endp X)
Y
(cons (car X)
(set-union (cdr X) Y))))
which returns
(PROGN
(DEFUN SET-UNION (X Y)
"SET UNION, I.E., X U Y"
(DECLARE (XARGS :GUARD (TRUE-LISTP X)))
(IF (ENDP X)
Y (CONS (CAR X)
(SET-UNION (CDR X) Y))))
(DEFTHM SET-UNION-RETURN-TYPE
(IMPLIES (TRUE-LISTP Y)
(TRUE-LISTP (SET-UNION X Y)))
:RULE-CLASSES :TYPE-PRESCRIPTION))
So defun-g takes an extra argument that appears after the
declaration and generates two events: a defun, as expected, and
the extra argument is turned into a defthm whose name is derived
from the defun.
Hint: Refer to the ACL2 online documentation for functions that manipulate symbols, the definition of true-listp, progn, defthm, etc.
Mechanized Formal Reasoning about Programs and Computing Machines, Bob Boyer and J Moore, in R. Veroff (ed.), Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1996. A pdf version is also available.
This paper explains a formalization style that has been extremely successful in enabling mechanized reasoning about programs and machines, illustrated in ACL2. This paper presents the so-called "small machine" model, an extremely simple processor whose state consists of the program counter, a RAM, an execute-only program space, a control stack and a flag. The paper explains how to prove theorems about such models.
Read up to the end of section 4.4 carefully and briefly skim the rest of the paper.
An ACL2 file with the relevant definitions can be found here.
Notice that what we have is a simulator for the small machine and what is interesting about the paper is that it then goes on to describe how one can state, prove, and mechanically verify theorems about the simulator.
Write a pair of functions fact-program and fact-clock so that for any natural number, n
(equal (car (mem (sm (fact-state n) (fact-clock n)))) (fact n))is a theorem, where fact and fact-state are defined as follows.
(defun fact (n) (if (zp n) 1 (* n (fact (1- n))))) (defun fact-state (n) (st :pc '(fact . 0) :stk nil :mem `(,n) :halt nil :code (list (times-program) (fact-program))))That is, (sm (fact-state n) (fact-clock n)) is a state with a memory whose first element is n! (n factorial). Times-program and the other functions appearing in the above expression are in the ACL2 file mentioned above. Try your solution with the following values for n: 7, 15, 22. You may have to compile your definitions if you run into stack overflows (type (comp t) at the command prompt). If your solutions are correct, then ACL2 should prove theorems of the following form (automatically).
(defthm fact-theorem-7 (equal (car (mem (sm (fact-state 7) (fact-clock 7)))) (fact 7)))
For this part of the project, submit your definitions of the functions fact-program and fact-clock and defthms fact-theorem-7, fact-theorem-15, fact-theorem-22, where fact-theorem-7 is as above and the other defthms are the same, except occurences of 7 are replaced by 15 and 22.