; Defspec for the Version of M1 with Stobjs ; J Strother Moore ; To recertify: ; (include-book "m1-with-stobj") ; (certify-book "m1-with-stobj-defspec" 1) ; Summary: In the paper ``Inductive Assertions and Operational Semantics,'' J ; Moore, CHARME 2003, D. Geist (ed.), Springer Verlag LNCS 2860, pp. 289-303, ; 2003, I describe how an operational semantics may be used directly to prove ; partial correctness via the Turing/Floyd-Hoare inductive assertion method, ; without resort to an external tool like a verification condition generator ; other than a theorem prover. In this book, I implement a macro for the ; method, specifically tailored proofs about the version of M1 defined with ; single-threaded objects. See the above mentioned paper for an explanation of ; what is going on here. In m1-with-stobj-defspec-example.lisp I use this ; utility to verify the partial correctness of a simple M1 program. (in-package "M1") (include-book "misc/defpun" :dir :system) (defmacro defpun (g args &rest tail) `(acl2::defpun ,g ,args ,@tail)) (defun how-many (e x) (if (endp x) 0 (if (equal e (car x)) (+ 1 (how-many e (cdr x))) (how-many e (cdr x))))) (defun find-pc (e x) (if (endp x) nil (if (equal e (car x)) 0 (if (find-pc e (cdr x)) (+ 1 (find-pc e (cdr x))) nil)))) (defthm lemma-for-halting-pc (implies (and (equal (how-many e x) 0) e) (not (equal (nth i x) e)))) (defthm halting-pc (implies (and (equal (how-many '(HALT) program) 1) (equal (nth i program) '(HALT))) (equal (nfix i) (find-pc '(HALT) program))) :rule-classes nil) (defthm program-never-changes (equal (rd :program (m1 s clk)) (rd :program s)) :hints (("Goal" :in-theory (enable m1 step)))) (in-theory (disable nth update-nth)) (defmacro defspec (name prog inputs pre-pc post-pc annotation-alist single-haltp) ; Single-haltp should be T only if there is exactly one HALT in prog and it is ; at post-pc. (let ((Inv (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-INV") 'm1)) (Inv-def (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-INV-DEF") 'm1)) (Inv-opener (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-INV-OPENER") 'm1)) (Inv-step (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-INV-STEP") 'm1)) (Inv-run (intern-in-package-of-symbol (concatenate 'string (symbol-name name) "-INV-RUN") 'm1)) (Correctness (intern-in-package-of-symbol (concatenate 'string "PARTIAL-CORRECTNESS-OF-PROGRAM-" (symbol-name name)) 'm1)) (Correctness-restated (intern-in-package-of-symbol (concatenate 'string "PARTIAL-CORRECTNESS-OF-PROGRAM-" (symbol-name name) "-RESTATED") 'm1))) `(progn (defpun ,Inv (,@inputs s) (if (member (pc s) ',(strip-cars annotation-alist)) (and (equal (program s) ,prog) (case (pc s) ,@annotation-alist)) (,Inv ,@inputs (step s)))) (defthm ,Inv-opener (implies (and (equal pc (pc s)) (syntaxp (quotep pc)) (not (member pc ',(strip-cars annotation-alist)))) (equal (,Inv ,@inputs s) (,Inv ,@inputs (step s))))) (defthm ,Inv-step (implies (,Inv ,@inputs s) (,Inv ,@inputs (step s)))) (defthm ,Inv-run (implies (,Inv ,@inputs s) (,Inv ,@inputs (m1 s clk))) :rule-classes nil :hints (("Goal" :in-theory (e/d (m1)(,Inv-def))))) (defthm ,Correctness (let* ((sk (m1 s0 clk))) (implies (and (let ((s s0)) ,(cadr (assoc pre-pc annotation-alist))) (equal (pc s0) ,pre-pc) ; ,@(equate-locals-with-inputs inputs 0) (equal (program s0) ,prog) (equal (pc sk) ,post-pc)) (let ((s sk)) ,(cadr (assoc post-pc annotation-alist))))) :hints (("Goal" :use (:instance ,Inv-run ,@(pairlis\$ inputs (acl2::pairlis-x2 inputs nil)) (s s0) (clk clk)))) :rule-classes nil) ,@(if single-haltp `((defthm ,Correctness-restated (implies (and ,(acl2::subst-var 's0 's (cadr (assoc pre-pc annotation-alist))) (equal (rd :pc s0) ,pre-pc) (equal (rd :program s0) ,prog) (equal sk (M1 s0 clk)) (haltedp sk)) ,(acl2::subst-var 'sk 's (cadr (assoc post-pc annotation-alist)))) :hints (("Goal" :use ((:instance ,Correctness) (:instance halting-pc (program *pi*) (i (rd :pc (m1 s0 clk)))))))) ) nil))))