Lärkfamilj

Larch -familjen av formella specifikationsspråk är avsedda för exakt specifikation av datorsystem. De tillåter rena specifikationer av datorprogram och formulering av bevis om programbeteende.

Larch-familjen utvecklades främst i USA på 1980- och 1990-talen, och involverade forskare vid Xerox PARC , DEC Systems Research Center (DEC/SRC), Massachusetts Institute of Technology (MIT) och andra platser. Till skillnad från Z-notationen har Larch-familjen ett språk för algebraisk specifikation av abstrakta datatyper ( Larch Shared Language (LSL)), och ett separat gränssnittsspråk skräddarsytt för varje språk som program ska skrivas på, såsom C , Modula -3 , Smalltalk , etc. Larch-projektet utvecklade också verktyg för att stödja användningen av formella specifikationer, inklusive Larch Prover (LP).

Se även

Formella metoder

externa länkar