Specificatie taal - Specification language

Een specificatietaal een formele taal in informatica tijdens systeemanalyses , requirements analyse en systemen te ontwerpen om te beschrijven op een veel hoger niveau dan een programmeertaal die wordt gebruikt om de uitvoerbare code te produceren voor een systeem.

Overzicht

Specificatietalen worden over het algemeen niet direct uitgevoerd. Ze zijn bedoeld om het wat te beschrijven , niet het hoe . Het wordt inderdaad als een fout beschouwd als een specificatie van een vereiste vol staat met onnodige implementatiedetails.

Een gemeenschappelijke fundamentele aanname van verschillende specificatie zal dat programma worden gemodelleerd als algebraïsche of model-theoretische structuren die een verzameling omvatten verzamelingen gegevenswaarden met functies over die sets. Dit abstractieniveau valt samen met de opvatting dat de juistheid van het input/output-gedrag van een programma voorrang heeft op al zijn andere eigenschappen.

In de eigenschapsgerichte benadering van specificatie (bijvoorbeeld door CASL ), bestaan ​​specificaties van programma's voornamelijk uit logische axioma's , meestal in een logisch systeem waarin gelijkheid een prominente rol speelt, die de eigenschappen beschrijven waaraan de functies moeten voldoen - vaak alleen door hun onderlinge relatie. Dit in tegenstelling tot de zogenaamde modelgerichte specificatie in frameworks als VDM en Z , die bestaan ​​uit een eenvoudige realisatie van het gewenste gedrag.

Specificaties moeten een proces van verfijning (het invullen van implementatiedetails) ondergaan voordat ze daadwerkelijk kunnen worden geïmplementeerd. Het resultaat van een dergelijk verfijningsproces is een uitvoerbaar algoritme, dat ofwel is geformuleerd in een programmeertaal, of in een uitvoerbare subset van de betreffende specificatietaal. Bijvoorbeeld Hartmann pijpleidingen , indien juist toegepast, kan worden beschouwd als een datastroom specificatie die is direct uitvoerbaar. Een ander voorbeeld is het actormodel dat geen specifieke applicatie-inhoud heeft en gespecialiseerd moet zijn om uitvoerbaar te zijn.

Een belangrijk gebruik van specificatietalen is het maken van bewijzen van programma-correctheid ( zie stellingbewijzer ).

Talen

Hoofdpagina: Categorie: Formele specificatietalen

Zie ook

Referenties

  1. ^ Joseph Goguen "One, None, honderdduizend specificatietalen" Invited Paper, IFIP Congress 1986 pp 995-1004
  2. ^ Fuchs, Norbert E.; Schwertel, Uta; Schwitter, Rolf (1998). "Attempto Controlled Engels - niet zomaar een andere logische specificatietaal" (PDF) . Internationale workshop over synthese en transformatie van logisch programmeren . Collegenota's in de informatica. 1559 . springer. blz. 1-20. doi : 10.1007/3-540-48958-4_1 . ISBN 978-3-540-65765-1.
  3. ^ Linden, Theodorus; Lawrence Markosian (1989). "Transformationele synthese met behulp van Verfijnen" . In Richer, Mark (red.). AI-hulpmiddelen en -technieken . Ablex. blz. 261-286. ISBN 0-89391-494-0. Ontvangen 6 juli 2014 .