[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

  1. Russell Turpin<turpin@cs.utexas.edu>
  2. A logical Approach to Data Structures
  3. In [Notkin93] pp138-148
      Part of Texas Adv Res Proj, admin J C Browne.

      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.


    1. PartOf(x,y),
    2. Dangles(p,x)::=p is not NULL but x has no part with address p,
    3. HasDangles(x), Navigable(x), Disjoint(y,x), y":"":"x

      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 [1] Beeri Catriel et al "Embedding Ψ- terms in a Horn-clause Logic Language" MCC Tech Report ACA-ST-050-88.

      objects See [12] 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 bibliographic items containing a matching string.

(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.

To see the complete bibliography (1Mb+) select:[Bibliography]