Graph Cloning in KIV

· Uncategorized
Author

An overview over the KIV project can be found here

The graph in the heap consists of nodes that store a value (of an unspecified element) and a map from the same element type to successors, that are given by references to the heap. The heap maps from references to nodes (it is instantiated here. The map from nodes to nodes thus maps references.

Specification functions contains several auxiliary definitions

  • A predicate closed that specifies that the heap is closed wrt. lookup of successor nodes
  • Injectivity of maps
  • An apply function that applies a map to a heap. Its purpose is to get the cloned part of the heap
  • A recursive definition of paths, i.e., lists of elements, and a derived predicate for reachability

Specification copy implements the cloning algorithm, and specification eval implements the eval procedure.

Solution

We have solved subchallenges 1 to 4 for copy and 1 to 3 for eval. Specifically, under the assumption that the heap is closed wrt. lookup we have proved

KIVs logic is total and access to non-allocated references in formulas yields unspecified results. The procedures readwritealloc that are defined in the library detect invalid heap access and abort in such a case. Hence, termination proves memory safety. In the same specification there is an axiom that postulates infinite memory (so allocation succeeds always).

The proofs are by induction, the measure is the size of the domain of the original heap minus the size of the map. Termination needs a fairly strong invarinat, that is specified in copy as two predicates copy-node-prepost and copy-edges-prepost. These predicates state that the current heap can be split disjointly into the original heap and a new part. The domain of the map is bounded by the new heap, whereas the range of the map corresponds to the new part. Furthermore, the two subheaps are closed on their own and the map is injective.

For eval, we prove

Since we don’t use integers, the success of eval is encoded by an option type with alternatives some/none. The proofs we have done for eval are trivial.

We have not proved that the copied graph is isomorphic. However, there is a theorem map-path in specification functions that states that for an injective map that contains at least the references reachable from the path in the originial sub-graph in its domain, the mapped path equi-exists.

Since we have proved that the map is injective, it remains to be shown that it is a homomorphism (it is surjective as well as its range is exactly the new heap).

Project Archive:

graph-cloning.tar

Leave a Comment