Topic: program proof via assertions

topics > computer science > programming > Group: program proving

automated tests of specifications and designs
consistency testing
constructing proof and program together
exceptions from invalid input
formal methods and languages
mathematical proof
model checker
predicate transforms
proof-carrying code
requirement specification by assertion
run-time assertions
safety, liveness, and system properties


Assertion proofs verify the equivalence of a program to assertions about the program's state. Although primarily an academic procedure, assertion proofs have been successful in critical portions of banking and military applications. Most widely known is Hoare's technique of surrounding operations with pre-and post-conditions, and proving that the program satisfies initial and final assertions. Hoare assertions usually include state variables (e.g., stack empty) for identifying the current condition of an object. Clarke (QuoteRef: clarEM1_1979) has found that a complete set of Hoare axioms can not be built for languages with procedure parameters, recursion, static scope, global scope, and internal procedures. Wulf (QuoteRef: wulfWA6_1976) designed the language Alphard specifically for assertion proofs. Redelmeier (QuoteRef: redeDH7_1979) includes assertions as part of a refinement's name. Assertion proofs require an additional termination proof. Manna (QuoteRef: mannZ5_1978) combines assertion and termination proofs by defining intermittent assertions for assertions which will be true at least once during program execution. (cbb 5/80)
Subtopic: correctness up

Quote: a data representation is correct if every procedure models the intended abstract operation and initialization models the abstract, initial value [»hoarCA_1972a]

Subtopic: proofs up

Quote: a proof is a set of correct assertions; use a proof system to keep track of proved and unproved assertions [»pratVR_1980]
Quote: proved correct ordering of partial records by inserting assertions at each control point; prevented sequencing errors [»vangR7_1978]
QuoteRef: kiebRB9_1973 ;;6.2 proves program by formal properties expressed in representation type
QuoteRef: hoarCA2_1974 ;;144 relational model--defined by axioms. theorems of true assertions on memory states before and after program execution
QuoteRef: goodDI_1974 ;; language with which to prove programs, using assertions and state changes
QuoteRef: shawM8_1976 ;;13 gives proof techniques for both for and first constructor

Subtopic: verification up

Quote: need predicate logic to reason effectively about specifications/programs for/of mechanisms [»hehnEC2_1984]
Quote: a program P is correct for specification S if P is as determined as S and every mechanism for P is also one for S [»hehnEC2_1984]
Quote: verification gives programmers a language for understanding the program as it is written; important explanations become assertions [»bentJ10_1983]
Quote: verify a program given input-output assertions by finding intermediate assertions and generating and proving verification conditions [»mannZ5_1978]
Quote: correct code by using sound principles during design, verification by analysis, and exhaustive testing of small cases [»bentJ10_1983]
Quote: proof-carrying code by computing the safety predicate and a checkable proof; Floyd's verification conditions [»necuGC10_1996]

Subtopic: hierarchical verification up

Quote: verify a program by verifying each component separately, checking consistency of specifications, and checking the program's requirements [»parnDL5_1988]
Quote: function-theoretic design verification for verifying successive function decompositions into control structures and subfunctions [»lingRC10_1988]
Quote: verify state-box descriptions by eliminating references to state data; should match the original black-box function [»cobbRH11_1990]
Quote: verify clear-box descriptions by eliminating references to lower level black boxes; should match the original state-box function [»cobbRH11_1990]
Quote: verify the expansion of a clear-box into code by constructing a proof argument that the expansion matches the functional specification [»cobbRH11_1990]
QuoteRef: shawM6_1976 ;;11 can prove correctness of form independent of other forms
QuoteRef: kiebRB9_1973 ;;1.1 separates definition of data structures from their use for proving

Subtopic: verification languages up

Quote: design of Euclid ensured that only local information was needed for verification [»veneT3_1978]
Quote: Alphard was designed for its verification technique [»wulfWA6_1976]
Quote: in Alphard, every function has concrete input and output assertions [»wulfWA6_1976, OK]
QuoteRef: wulfWA6_1976 ;;19 Alphard defines abstract states (eg empty stack) for describing different predicates
QuoteRef: wulfWA6_1976 ;;9 specification consists of abstract invariant, required properties of parameters, initial value properties, input/output relations for each abstract operation
QuoteRef: wulfWA6_1976 ;;10 Wulf's proof method: prove that abstract and concrete representations are consistent and the pre-post conditions hold across operations

Subtopic: specification up

Quote: functional verification structures a proof that a program implements its specification correctly [»cobbRH11_1990]
Quote: describe a program by its input and output specification [»mannZ7_1979]

Subtopic: preconditions and post-conditions up

Quote: a procedure's correctness may depend on a set of preconditions; must be proved to hold before every call [»hoarCA_1972a]
Quote: describe a routine accurately; include preconditions, postconditions, validity conditions, accuracy, time taken, and method [»turiA3_1951]
Quote: specify postcondition in an ensures clause; use "#" prefix to indicate the previous value [»harmDE5_1991]
Quote: verify a subroutine by its pre and postconditions; if preconditions satisfied then postconditions will be after execution [»bentJ10_1983]
Quote: the name of a refinement includes its precondition, its assignments to global variables, and an optional postcondition [»redeDH7_1979]
Quote: Hoare axioms exist for at most 4 of 5 block-structured features: procedure parameters, recursion, static scope, globals, internal procedures [»clarEM1_1979]
Quote: dependency specification better than dependency graph; no transitivity problem, allows polymorphism, supports pre- and post-conditions, enables substitutivity [»jackD10_2002]
QuoteRef: shawM6_1976 ;;5 uses pre and post conditions all over
QuoteRef: wulfWA6_1976 ;;9 Hoare '69: pre-condition (y) {operation} post-condition (y)

Subtopic: assertions and invariants up

Quote: a data representation has an invariant condition that is instantiated at initialization and preserved by each operation [»hoarCA_1972a]
Quote: proving program correctness depends on knowing the invariants satisfied by the program; given a complicated program may be difficult to find [»baueFL_1976]
Quote: a class maintains an invariant, i.e., a piece of code that checks the state of an object
Quote: in a well-defined class, an initialized object satisfies a simple invariant that is maintained by all operations until the object is destroyed
Quote: a mutex protects the invariant of the associated data; restore the invariant before calling Wait or Signal [»birrAD_1991]
Quote: prove banking system by proving invariants: what was sent equals what was received, and vice versa [»vangR7_1978]
Quote: an intermittent assertion holds at least once when control is at that point [»mannZ5_1978]
Quote: constraints for which operations for an entity, static and dynamic invariants, and pre-/ post-conditions [»smitJM1_1981]
QuoteRef: robiL9_1975 ;;3 global assertions - true at initial state and any sequence of operations afterwards
Quote: a multi-exit statement includes labels for alternative actions and assertions for program proving [»backRJ11_1979, OK]

Subtopic: loop invariant up

Quote: a loop is correct if the loop invariant is established by initialization and preserved each iteration; also prove final result and termination [»bentJ10_1983]
Quote: it is important to find the loop invariant for each loop [»grieD_1981]
Quote: every loop should have a proof for termination and a loop invariant [»dijkEW10_1972]
Quote: eliminate proofs of termination by avoiding loop forever constructs [»andeT_1985]

Subtopic: temporal logic up

Quote: used a model checker to verify safety assertions written in temporal logic; found subtle discrepancies [»atleJM1_1993]

Subtopic: annotations up

Quote: for alias burying, annotate parameters, return values, and fields as unique or borrowed; restricts use; need to analyze local variables [»boylJ5_2001]

Subtopic: algebraic specification up

QuoteRef: guttJV12_1974 ;;54 dyadic specification by operations and axioms-- i.e. an algebraic system
QuoteRef: guttJV12_1974 ;;56 specification by operations and axioms eg attributes (initialize symbol table, id)= error. Attributes (add (symbol table, id, attributes), id') -if ?equal? (id, id') the attributes else Attributes (sym tab, id')

Subtopic: example execution up

Quote: add assertions which give the correct result for an example execution; machine-checked; made program easier to understand [»morrJH_1980]

Subtopic: examples up

Quote: used assertions to improve the reliability and correctness of real software at Chase Manhattan Bank [»vangR7_1978]
Quote: proof of Smallintset using loop invariant and postcondition [»hoarCA_1972a]

Subtopic: use name as specification up

Quote: while proving a refinement, assume that a call does what its name promises
Quote: a refinement's name is also its precise specification; so prove that refinement matches its name [»redeDH7_1979]

Subtopic: difficulty of assertion proof up

Quote: the details of the proof of Smallintset are complex and not included with this paper

Related Topics up

Topic: automated tests of specifications and designs (12 items)
Topic: consistency testing (60 items)
Topic: constructing proof and program together (22 items)
Topic: exceptions from invalid input (4 items)
Topic: formal methods and languages (53 items)
Topic: mathematical proof (23 items)
Topic: model checker (49 items)
Topic: predicate transforms (7 items)
Topic: proof-carrying code (7 items)
Topic: requirement specification by assertion (28 items)
Topic: run-time assertions (25 items)
Topic: safety, liveness, and system properties
(22 items)

Updated barberCB 11/04
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.