This page documents our solutions to the problems of the Verified Software Competition (VSCOMP) 2014.

Problem 1 - Patience Solitaire

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).

Problem 2: Partition Refinement

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.

Implementation

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: first, last, and count. Therefore in our formalization, a partition is just a list of partelems.

Test

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:

This test can be found in specification partition-refinement-test. Theorem MAIN-example proves that the algorithm yields the expected result. The "test-proof" uses lemmas REFINE-example and NEWPARTS-example which describe the results of the two procedures used by the MAIN-routine for the given concrete input. The symblic execution of the program for the concrete input is almost automatic, given a couple of strong simplifier rules.

Formalization of properties

We use a couple of predicates and functions to express the proof obligation and the invariants for the while-loops. These predicates and functions are defined in specification partition-refinement. Their signatures are defined in the sections "functions" and "predicates", the axioms are in the "axiom" section. Most important are:

Verification Task

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".

Problem 4: Graph Cloning

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

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 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).

[Imprint] [Data Privacy Statement] [E-Mail]