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 […]
Category archives for Uncategorized
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 […]
This is a complete solution to problem 4 in Dafny. Task 1 is implemented in the method Node.Copy. Requirements are verified as follows: Dafny checks absence of runtime errors. Dafny checks termination. Postcondition (b) of Copy. Since Copy has an empty modifies clause (default), Dafny check the absence of side effects. Postconditions (a), (c) and […]
The solution to this problem is written in Isabelle2013-2. The solution is a collection of primitive recursive functions. The Isabelle theory files are here: Problem2. There are 3 files: PartitionAlgorithm.thy – the implementation of the algorithm PartitionProofs.thy - The definitions of the invariants and all proofs PartitionTasks.thy – The proofs for the tasks.