An algorithm for generating weakest preconditions as mutually recursive functions.
This book generates weakest precondition predicates, which are admitted as (possibly mutually recursive) ACL2 functions as described in the paper A Weakest Precondition Model for Assembly Language Programs by Bill Legato, dated January 28, 2003.
The input program is given in a variation of Legato's format for assembly language programs. In this format each node of the program (where node roughly corresponds to program line) is represetned as a sequential substitution defining updates to state. Presently, state variables are inferred from the given substitutions and predicates and all functions are given as functions of full state with irrelevant-formals ignored.
No particular program language is required. The right hand side of a
substitution can be any function defined in the current ACL2 logical world,
although we typically think of these operations as being low-level or
primitive. Many of the examples provided with the book use pcode operations,
for which a partial semantics has been provided in
Here main is the program to be analyzed, in the format as specified below in the section Program Format. (Also, see examples directory for some sample programs).
A user of this book will generally want to specify one or more of the following options.
A program consists of a list of nodes in the following format.
(:node :label idx :pre annot-pre :subst sub :branches ((pred1 . idx1) ... (predn . idxn)) :post annot-post)
To generate a list of WP functions without admitting them, use run-wp-list:
(run-wp-list main prefix count-var mutrec prog-mode)
(include-book "wp-gen") (ld "examples/new-program.lisp") (run-wp-list (@ new-prog) 'wp-new1 'count t nil)
(MUT-REC (DEFUN WP-NEW1-L_1 (U V W COUNT) (DECLARE (XARGS :MEASURE (ACL2-COUNT COUNT))) (IF (ZP COUNT) NIL (WP-NEW1-L_2 U (INT_XOR U 12345 32) W (- COUNT 1)))) (DEFUN WP-NEW1-L_2 (U V W COUNT) (DECLARE (XARGS :MEASURE (ACL2-COUNT COUNT))) (IF (ZP COUNT) NIL (WP-NEW1-L_3 U V (INT_ADD V 2345345299 32) (- COUNT 1)))) (DEFUN WP-NEW1-L_3 (U V W COUNT) (DECLARE (XARGS :MEASURE (ACL2-COUNT COUNT))) (IF (ZP COUNT) NIL (OR (AND (NOT (= (INT_EQUAL W 8281919193 32) 1)) (WP-NEW1-L_END U V W (- COUNT 1))) (AND (= (INT_EQUAL W 8281919193 32) 1) (WP-NEW1-L_BAD U V W (- COUNT 1)))))) (DEFUN WP-NEW1-L_BAD (U V W COUNT) (DECLARE (XARGS :MEASURE (ACL2-COUNT COUNT))) (IF (ZP COUNT) NIL T)) (DEFUN WP-NEW1-L_END (U V W COUNT) (DECLARE (XARGS :MEASURE (ACL2-COUNT COUNT))) (IF (ZP COUNT) NIL NIL)))
Note: This form will generate an error from ACL2 as given, because it contains irrelevant formals.
Please direct questions/comments/bugs to Sarah Weissman (email@example.com).
Except where otherwise specified this is a work of the U.S. Government and is not subject to copyright protection in the United States. Foreign copyrights may apply.
This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA.