| 
|
QuoteRef: hoarCA_1972a
Topic:
abstract data type
Topic:
program proof via assertions
Topic:
representation data type
Topic:
program proving is infeasible
Reference
Hoare, C.A.R., "Proof of correctness of data representations", Acta Informatica, 1, pp. 271-281, 1972. Google
Other Reference
page numbers from Broy, M., Denart, E. (ed), Software Pioneers, Springer, 2002, p. 386-396
390 ;;Quote: a data representation is correct if every procedure models the intended abstract operation and initialization models the abstract, initial value
390 ;;Quote: a data representation has an invariant condition that is instantiated at initialization and preserved by each operation
390 ;;Quote: a procedure's correctness may depend on a set of preconditions; must be proved to hold before every call
392 ;;Quote: proof of Smallintset using loop invariant and postcondition
392 ;;Quote: the details of the proof of Smallintset are complex and not included with this paper
Topic: abstract data type (64 items)
Topic: program proof via assertions (61 items)
Topic: representation data type (21 items)
Topic: program proving is infeasible (47 items)