Beispiel eines SPARK Programms: Der „Global“ Vertrag spezifiziert, dass die Implementation von „Insert“ die Variable „T“
Beispiel eines SPARK Programms: Der „Global“ Vertrag spezifiziert, dass die Implementation von „Insert“ die Variable „T“ sowohl lesen als auch schreiben wird. Die „Pre“ Vorbedingung muss bei jedem Aufruf von „Insert“ erfüllt werden: „T“ soll nicht voll sein und soll nicht bereits den einzufügenden Wert enthalten. Die „Post“ Nachbedingung ist die Eigenschaft die „Insert“ selbst garantiert: der as „Item“ überreichte Parameter ist dann in „T“ enthalten. Die SPARK Werkzeuge können dazu verwendet werden, diese Verträge zu überprüfen: dass T wie spezifiziert in „Insert“ benutzt wird (und keine anderen globalen Variablen), dass alle Aufrufe von „Insert“ die Vorbedingung erfüllen, und dass „Insert“ seine Nachbedingung erfüllt. ( Bild: Adacore )