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.
Auteurs: Claire Dross
Catégories: Array Data Structure
Outils: SPARK 2014
Références: 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.