[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Formal development and verification of data structure programs. pointers and destructive update.
"well known to programmers but they are usually informally defined by the programming community or operationally defined in particular imperative languages" NO!: implementations. Concepts: data structures address, pointer reference, data structure disjointness, data structure isomorphism.
"gap between the formalisim that was provided and the way in which the problem area is naturally discussed... common textx on formal verification omit pointers from their prescription for programming.
Status: prototype compiler, graphical interface, mapping to standard theprem prover, incomplete....environment enforces a greater attention to invariants, details, and exceptional conditions. Debugging moved to compile time. out-of-bounds suscripts and mangled pointers are eliminated.
records See  Beeri Catriel et al "Embedding Ψ- terms in a Horn-clause Logic Language" MCC Tech Report ACA-ST-050-88.
objects See  MaierD86, "A Logic for Objects" In Proc o t Workshop on the Foundations of Deductive Databases and Logic Programming, Washington DC, Aug 1986 pp6-26.
Galois programs specified in logic: name, modes for arguments, goal predicate, precondition - no unification or clausal search required. Composition generates proof obligations: Prerequisite asssertion
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]