Authors
Rüdiger Lunde, Claus-Peter Wirth
Title
ASF+   -   eine ASF-ähnliche Spezifikationssprache
In
SEKI Working Paper SWP-94-05, Univ. Kaiserslautern, 1994
Bib Entry
Abstract
German
Ohne auf wesentliche Aspekte der in [Bergstra&al.89] vorgestellten algebraischen Spezifikationssprache ASF zu verzichten, haben wir ASF um die folgenden Konzepte erweitert: Waehrend in ASF einmal exportierte Namen bis zur Spitze der Modulhierarchie sichtbar bleiben muessen, ermoeglicht ASF+ ein differenziertes Verdecken von Signaturnamen. Das fehlerhafte Vermischen unterschiedlicher Strukturen, welches in ASF beim Import verschiedener Aktualisierungen desselben parametrisierten Moduls auftritt, wird in ASF+ durch eine adaequatere Form der Parameterbindung vermieden. Das neue Namensraum-Konzept von ASF+ erlaubt es dem Spezifizierer, einerseits die Herkunft verdeckter Namen direkt zu identifizieren und anderseits beim Import eines Moduls auszudruecken, ob dieses Modul nur benutzt oder in seinen wesentlichen Eigenschaften veraendert werden soll. Im ersten Fall kann er auf eine einzige global zur Verfuegung stehende Version zugreifen; im zweiten Fall muss er eine Kopie des Moduls importieren. Schliesslich erlaubt ASF+ semantische Bedingungen an Parameter und die Angabe von Beweiszielen.
English
Maintaining the main aspects of the algebraic specification language ASF as presented in [Bergstra&al.89] we have extend ASF with the following concepts: While once exported names in ASF must stay visible up to the top the module hierarchy, ASF+ permits a more sophisticated hiding of signature names. The erroneous merging of distinct structures that occurs when importing different actualizations of the same parameterized module in ASF is avoided in ASF+ by a more adequate form of parameter binding. The new ``Namensraum''-concept of ASF+ permits the specifier on the one hand directly to identify the origin of hidden names and on the other to decide whether an imported module is only to be accessed or whether an important property of it is to be modified. In the first case he can access one single globally provided version; in the second he has to import a copy of the module. Finally ASF+ permits semantic conditions on parameters and the specification of tasks for a theorem prover.
Full paper