This page documents our solutions to the problems of the Verified Software Competition (VSCOMP) 2014.
An overview over the KIV project can be found here
The problem is formulated algebraically. The entire axiomatization can be found in the specification solitaire. The game is formalized as the function solitaire, which returns the list of stacks after distributing all cards over the stacks, with the helper function push. The latter recurses over the stacks and prepends to the first stack where this is possible.
The idea of the proves is to switch the representation, i.e., we use the function solix, which returns the stack of indices (into the original sequence) instead of the cards themselves.
The first theorem solix-to-solitaire states that we can obtain the result of solitaire by calculating solix of the same cards and then replacing the indices in the stacks by the actual elements. This conversion is done by the function .tolist.
This allows us to prove the main theorem
by proving the same theorem (found here) over the stack of indices. The proof of this theorem follows the description given by the organizers
of the competition, i.e., the proof is decomposed into
A few properties about the result of solix are needed throughout the proofs and are defined by the predicates inv (stacks are nonempty and all indices are within the bounds of the original sequence), covers (all indices are covered by the resulting list of stacks) and ordered (the indices within each stack are ordered and the corresponding elements are also ordered).
An overview over the KIV project can be found here. Orange specifications in the project structure graph are imported from KIV's library, the green specifications are problem specific additional specifications. The green color indicates that all proof obligations are done and the proofs are in a consistent state.
The implementation of the algorithm can be found in specification partition-refinement.It consists of the procedures MAIN, REFINE, REFINEONE,and NEWPARTS. Procedure MAIN implements the whole algorithm and uses procedures REFINE and NEWPARTS. REFINE iterates over X and calls REFINEONE for each x ∈ X. This is the first phase of refine(A,D,P,F,X) as given in step 1 of the algorithm description in the problem description. REFINEONE is our implementation of refineOne(A,D,P,F,x) from step 2 of the algorithm description in the problem description. NEWPARTS is our implementation of makeNewPartitions(P,F) from step 3 of the algorithm description in the problem description. MAIN implements refine(A,D,P,F,X) as given in the problem description by first calling REFINE for phase one and then NEWPARTS for phase two.
Our algorithm works on algebraically specified data types for arrays, lists, sets, natural numbers, and maps. Those basic data types are all provided by KIV's rich library of predefined data types. Specifications taken from the library appear orange in the project structure graph on the project overview. We added one algorithm-specific data type called partelem. It represents one element of a partition (i.e. one intervall ) and consists of three parts:
Before starting the verification, we tested our implementation with the example given in the problem description. We symbolically executed our implementation for the concrete inputs:
The main proof obligation is theorem MAIN-theorem. It shows the termination of the algorithm (by proofing <MAIN(X; A, D, P, F)>φ which is a DL-formula that means total correctness) and it shows proof obligations 2.a (encoded in the predicate Fok(F, P, # A) of the post condition φ) and 2.b (encoded in the predicate partitionRefinement(P, A, P0, A0, X) of the post condition φ). The full postcondition φ that we prove in theorem MAIN-theorem is ( perm(A0, A) ∧ partitions(P, # A) ∧ divides(P, P0, X, A) ∧ DAid(A, D) ∧ ADid(A, D) ∧ Fok(F, P, # A) ∧ partitionRefinement(P, A, P0, A0, X))
The invariant for the while-loop in procedure REFINE can be found in the "Rule argument"-section on the page for proofstep for the "invariant right"-rule" of theorem REFINE-theorem. In the downloadable tgz of the project, this invariant can be found in the file "specs/partition-refinement/formulas.utf8". It is named "REFINE-INV".
The invariant for the while-loop in procedure NEWPARTS can be found in the "Rule argument"-section on the page for proofstep for the "invariant right"-rule" of theorem NEWPARTS-theorem. In the downloadable tgz of the project, this invariant can be found in the file "specs/partition-refinement/formulas.utf8". It is named "NEWPARTS-INV".
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
closed that specifies that the heap is closed wrt. lookup of successor nodesapply function that applies a map to a heap. Its purpose is to get the cloned part of the heapSpecification copy implements the cloning algorithm, and specification eval implements the eval procedure.
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 read, write, alloc 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).