Rüdiger Lunde, Claus-Peter Wirth

• Ohne auf wesentliche Aspekte der in [Bergstra&al.89] vorgestellten alge-braischen Spezifikationssprache ASF zu verzichten, haben wir ASF um die folgenden Konzepteerweitert: Während in ASF einmal exportierte Namen bis zur Spitze der Modulhierarchie sichtbarbleiben müssen, ermöglicht ASF + ein differenziertes Verdecken von Signaturnamen. Das fehlerhafteVermischen unterschiedlicher Strukturen, welches in ASF beim Import verschiedener Aktualisie-rungen desselben parametrisierten Moduls auftritt, wird in ASF + durch eine adäquatere Form derParameterbindung vermieden. Das neue Namensraum_Konzept von ASF + erlaubt es dem Spe-zifizierer, einerseits die Herkunft verdeckter Namen direkt zu identifizieren und anderseits beimImport eines Moduls auszudrücken, ob dieses Modul nur benutzt oder in seinen wesentlichen Ei-genschaften verändert werden soll. Im ersten Fall kann er auf eine einzige global zur Verfügungstehende Version zugreifen; im zweiten Fall muß er eine Kopie des Moduls importieren. Schließlicherlaubt ASF + semantische Bedingungen an Parameter und die Angabe von Beweiszielen.