## Cartesian Trees (from VerifyThis 2019) in SPARK

This program is a solution to the second challenge of VerifyThis 2019. For a sequence of distinct numbers S, the Cartesian tree of S is the only binary tree T such that T contains a node per element of S, T has the heap property, and symmetrical traversal of T encounters elements in the order of S. The challenge is split in two parts, first construct all nearest smaller neighbors to the left/right of each element of a sequence using a stack, and then construct the Cartesian tree of the sequence using these neighbors.

Computation of the nearest smaller neighbors is fairly straightforward in SPARK. It still features a relatively involved loop invariant. On the other hand, showing that the tree constructed by the algorithm in the second part is the Cartesian tree of the input sequence is rather involved. It uses ghost code to manually guide automatic solvers.

**Authors:** Claire Dross

**Topics:** Ghost code / Data Structures / Trees

**Tools:** SPARK 2014

**References:** ProofInUse joint laboratory / VerifyThis @ ETAPS 2019

**See also:** VerifyThis 2019: Cartesian trees

see also the index (by topic, by tool, by reference, by year)

download ZIP archive

The full code is in the ZIP archive above. Here are below the specifications. The proofs can be replayed using SPARK Community 2018 and invoking the

`test.cmd`script from the archive.