Wiki Agenda Contact Version française

Longest common prefix, in SPARK

SPARK 2014 - Longest_Common_Prefix Example

This example illustrates the use of Pre, Post and Contract_Cases aspects in SPARK 2014.


Authors: Claire Dross

Topics: Array Data Structure

Tools: SPARK 2014

References: ProofInUse joint laboratory

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 is below the specification. The proofs can be replayed using SPARK Community 2018 and invoking the test.cmd script from the archive.