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: first, last, and count. Therefore in our formalization, a partition is just a list of partelems.
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:
- A = mkarray(6)[0, 22][1, 33][2, 100][3, 55][4, 44][5, 11]
- D = (Ø)[100, 2][11, 5][22, 0][33, 1][44, 4][55, 3]
- P = pe(0, 2, 0) + pe(3, 5, 0) + 
- X = 11 + 22 + 44 + 
- F = (Ø)[0, 0][1, 0][2, 0][3, 1][4, 1][5, 1]
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:
- partitionRefinement: Expresses that each new partition p is either ⟦p0⟧(A) ∩ X or ⟦p0⟧(A) \ X for an old partition p0.
- Fok: Expresses that each array index n is mapped by F to a partition index F[n] such that interval P[F[n]] contains n.
- XornoX(p, X, A) expresses that the array elements indicated by intervall p are either only elements contained in X or do not contain any elements that are in X.
- partitions(P, n): States that a partition P is a proper partition for an array of size n, i.e. each array index is in an intervall contained in P and no index is contained in two different partitions.
- DAid(A, D): Expresses that D is an “inverse” of A.
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”.