Topic: automated tests of specifications and designs
Topic: consistency testing
Topic: constructing proof and program together
Topic: exceptions from invalid input
Topic: formal methods and languages
Topic: mathematical proof
Topic: model checker
Topic: predicate transforms
Topic: proofcarrying code
Topic: requirement specification by assertion
Topic: runtime assertions
Topic: safety, liveness, and system properties
 
Summary
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 preand postconditions, 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
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
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 modeldefined 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
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 inputoutput 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: proofcarrying code by computing the safety predicate and a checkable proof; Floyd's verification conditions [»necuGC10_1996]
 Subtopic: hierarchical verification
Quote: verify a program by verifying each component separately, checking consistency of specifications, and checking the program's requirements [»parnDL5_1988]
 Quote: functiontheoretic design verification for verifying successive function decompositions into control structures and subfunctions [»lingRC10_1988]
 Quote: verify statebox descriptions by eliminating references to state data; should match the original blackbox function [»cobbRH11_1990]
 Quote: verify clearbox descriptions by eliminating references to lower level black boxes; should match the original statebox function [»cobbRH11_1990]
 Quote: verify the expansion of a clearbox 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
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 prepost conditions hold across operations
 Subtopic: specification
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 postconditions
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 blockstructured 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 postconditions, enables substitutivity [»jackD10_2002]
 QuoteRef: shawM6_1976 ;;5 uses pre and post conditions all over
 QuoteRef: wulfWA6_1976 ;;9 Hoare '69: precondition (y) {operation} postcondition (y)
 Subtopic: assertions and invariants
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 welldefined 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/ postconditions [»smitJM1_1981]
 QuoteRef: robiL9_1975 ;;3 global assertions  true at initial state and any sequence of operations afterwards
 Quote: a multiexit statement includes labels for alternative actions and assertions for program proving [»backRJ11_1979, OK]
 Subtopic: loop invariant
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
Quote: used a model checker to verify safety assertions written in temporal logic; found subtle discrepancies [»atleJM1_1993]
 Subtopic: annotations
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
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
Quote: add assertions which give the correct result for an example execution; machinechecked; made program easier to understand [»morrJH_1980]
 Subtopic: examples
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
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
Quote: the details of the proof of Smallintset are complex and not included with this paper [»hoarCA_1972a]

Related Topics
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: proofcarrying code (7 items)
Topic: requirement specification by assertion (28 items)
Topic: runtime assertions (25 items)
Topic: safety, liveness, and system properties (22 items)
