Wiki Agenda Contact English version

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.