Attempto - Englisch als (formale) Spezifikationssprache (system description) by Norbert E. Fuchs, Üta Schwertel und Rolf Schwitter Üniversität Zürich, Schweiz Abstract An Spezifikationssprachen werden viele - zum Teil sogar widersprüchliche - Anforderungen gestellt. Einerseits sollen die Konzepte eines Anwendungsbereiches einfach und unmittelbar darg- estellt werden können, was für informelle Spezifikationen in natürlicher Sprache und in gra- phischen Notationen spricht, andererseits sollen formale Spezifikationen die Verifikation und die Validierung erleichtern und den Ausgangspunkt für eine möglichst automatische Programment- wicklung bilden. Das Attempto Spezifikationssystem überwindet diesen Widerspruch, indem es zwei semantisch äquivalente Darstellungen einer Spezifikation zur Verfügung stellt - eine in kon- trollierter natürlicher Sprache und eine in Prädikatenlogik. In Attempto Controlled English (ACE) - einer Teilmenge der englischen Sprache mit einge- schränkter Grammatik und problemspezifischem Vokabular - können Anwendungsspezialisten Spezifikationen direkt in den Konzepten des Anwendungsbereiches entwickeln [Fuchs & Schwit- ter]. ACE ist eine mächtige Sprache, in der modellorientierte und eigenschaftsorientierte Spezi- fikationen eindeutig und klar geschrieben werden können. Die Sprache ACE ist gleichzeitig so einfach, dass sie effizient von einem Computer verarbeitet werden kann. Üm das Erlernen und den Gebrauch der Sprache zu erleichtern, beruht ACE auf einer kleinen An- zahl von Prinzipien. Hier sind einige dieser Prinzipien: einfache Sätze werden durch eine kleine Anzahl von Konstruktoren (z.B. Negation, if-then, Konjunktion, Quantifizierung) zu komplexen Sätzen kombiniert; Verben werden nur in der dritten Person Präsens und nur aktiv gebraucht; es gibt keine modalen Verben (z.B. can, may). Das interaktive Attempto Spezifikationssystem über- setzt ACE Spezifikationen eindeutig in Diskursrepräsentationsstrukturen - eine syntaktische Vari- ante der Prädikatenlogik. Bei der Übersetzung werden Ellipsen und anaphorische Bezüge nach vorgegebenen Prinzipien aufgelöst. Gleichzeitig wird automatisch eine Paraphrase in ACE erzeugt, die den Benutzern zeigt, wie das Attempto System die Eingabe interpretiert hat. In einem zweiten Schritt können Diskursrepräsentationsstrukturen in Prolog übersetzt werden. Die in Logik übersetzte Spezifikation stellt den spezifizierten Sachverhalt formal dar. Man kann sich über diesen Sachverhalt orientieren, indem man einfache Fragen in ACE stellt, die durch lo- gische Inferenz beantwortet werden. Die übersetzte Spezifikation kann ausgeführt und die Aus- führung in ACE beobachtet und überprüft werden. Das führt dazu, dass Benutzer die Spezifikation in anwendungsspezifischen Konzepten validieren können. Das Attempto System stellt den Benutzern weitere Werkzeuge zur Verfügung, z.B. einen lexika- lischen Editor für den inkrementellen Aufbau des Lexikons und einen Spelling Checker, der das Schreiben korrekter Spezifikationen unterstützt. In ACE wurden bisher ein Geldautomat und eine kleine Datenbank für eine Bibliothek spezifiziert.