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

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

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]

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

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

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]

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)

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]

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]

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

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

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')

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

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]

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]

Quote: the details of the proof of Smallintset are complex and not included with this paper [»hoarCA_1972a]