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.