PVS (Prototype Verification System) ist ein Spezifikations- und Verifikationssystem mit integriertem interaktivem Theorembeweiser, entwickelt am SRI International; es basiert auf typisierter Higher-Order-Logik und wird besonders bei der NASA (Langley) für Hardware- und Protokoll-Verifikation eingesetzt. Eine Spezifikation besteht aus Theorien in .pvs-Dateien.

Arbeiten mit Theorien

pvs                    # Emacs-Oberflaeche starten
M-x typecheck          # Theorie typisieren (C-c C-t)
M-x prove              # Formel im Beweiser bearbeiten (C-c C-p)
M-x typecheck-prove    # Typecheck + Beweis in einem Schritt (tcp)

Eine Theorie definiert Typen, Konstanten und Axiome; Lemmata und Theoreme werden mit THEOREM bzw. LEMMA deklariert und mit Taktiken bewiesen.

Beweisführung im Prover

• prove-it: Komplettbeweis aller offenen Beweisziele („autopilot“).
• grind: Standard-Mischung aus Vereinfachen, Suchen und Auto-Beweis — der wichtigste Allround-Befehl.
• simplify: Formel propositional vereinfachen.
• (skolem!)/flatten: Quantoren instanziieren bzw. Konjunktionen/Implikationen auflösen.
• (assert): Entscheidbare Teile (Arithmetik, Gleichheit) automatisch schließen.
• quit: Beweissitzung verlassen; Beweise landen als .prf-Dateien neben der Theorie.

PVS ist eng verwandt mit anderen Formale-Verifikations-Werkzeugen wie Coq, Lean und Isabelle; mit VDM teilt es die Idee der formalen Spezifikation vor der Implementierung.

Gosu ist eine statisch typisierte, objektorientierte Sprache für die Java Virtual Machine (JVM). Sie entstand 2002 intern bei Guidewire Software für Versicherungsanwendungen und wurde 2010 als Open Source veröffentlicht. Gosu kombiniert Java-, C#- und ECMAScript-Ideen und ist vor allem im Versicherungsumfeld (P&C) verbreitet.

Dateien und Werkzeuge

• .gs – Gosu-Quelldatei; eine Klasse pro Datei, Name der Datei = Name der Klasse
• .gst – Gosu-Template-Datei (HTML-artige Templates mit Gosu-Ausdrücken)
• gosuc – Gosu-Compiler (Kommandozeile, kompiliert .gs nach Java-Bytecode)
• gosu – Interpreter/REPL für schnelle Experimente

Syntax-Grundlagen

package example
uses java.util.List

class Hallo {
  function gruesse(name : String) : String {
    var text : String = "Hallo " + name
    return text
  }
}

• uses – Import-Deklaration (statt import)
• var – lokale Variable, var x = 5 mit Typinferenz
• function f(p : Typ) : Rueckgabe – Methoden-Definition
• String-Templates: "Hallo ${name}" als First-Class-Sprachfeature

Praxis-Tipps

• Gosu bietet auch funktionale Elemente (Lambdas, Block-Expressions) und erweiterbare Typen (Enhancements) für bestehende Java-Klassen
• Dr. Dobb's Journal nominierte Gosu 2011 zur „Language of the Month“

Verwandte JVM-Sprachen: Java-Befehle, Kotlin-Befehle, Groovy-Befehle, C#-Befehle. Weitere JVM-Nachbarn: Xtend-Befehle und X10-Befehle.

Xtend ist eine statisch typisierte Programmiersprache aus dem Eclipse-Umfeld (Xtext-Projekt), die zu lesbarem Java-Quellcode kompiliert. Sie begann als „Xtend2“ und wurde mit Eclipse Juno (Juni 2012) ein eigenständiges Projekt. Xtend erweitert Java um moderne Sprachfeatures, ohne die JVM-Kompatibilität zu verlieren.

Kompilierung

• Quelldateien: .xtend, eine Klasse pro Datei
• Der Compiler erzeugt Java-Quellcode im Ordner xtend-gen, der dann normal von javac weiterverarbeitet wird
• Eclipse: Xtend-Plugin (Eclipse Update Site, Editor + Compiler integriert)
• Maven: xtend-maven-plugin mit Goal xtend:compile (bzw. xtend:testCompile)
• Gradle: Plugin org.xtext.xtend, Abhängigkeit org.eclipse.xtend:org.eclipse.xtend.lib

Syntax-Highlights

class Hallo {
  def String gruesse(String name) {
    val text = "Hallo " + name
    return text
  }
}

• def – Methoden-Definition (kompiliert zu Java-Methoden)
• val – unveränderliche Variable, var – veränderliche Variable; Typinferenz inklusive
• Lambdas: list.map[ it.length ] mit implizitem it
• Extension Methods: "hallo".toFirstUpper erweitert geschlossene Typen ohne Vererbung
• Active Annotations: Annotationen nehmen zur Übersetzungszeit am Kompilierungsprozess teil (Boilerplate-Erzeugung, z. B. für Visitor- oder Observer-Muster)
• Template-Expressions: mehrzeilige Strings mit «ausdruck»-Interpolation

Praxis-Tipps

• Da Xtend nach Java übersetzt wird, bleiben Debugging (mit Debug-Informationen) und Bibliotheksnutzung unkompliziert
• Kein separater Standalone-Compiler: Aufbau über IDE, Maven oder Gradle

Verwandte JVM-Sprachen: Java-Befehle, Kotlin-Befehle, Groovy-Befehle, Scala-Befehle. Weitere JVM-Nachbarn: Gosu-Befehle und X10-Befehle.

X10 ist eine statisch typisierte, objektorientierte Sprache für paralleles und verteiltes Rechnen, entwickelt von IBM am Thomas J. Watson Research Center im DARPA-Projekt PERCS (High Productivity Computing Systems). X10 erweitert einen sequenziellen Sprachkern um places (Orte), activities (Aktivitäten), clocks (Uhren) und verteilte Arrays – das sogenannte APGAS-Modell (Asynchronous Partitioned Global Address Space).

Werkzeuge

• x10c – Compiler mit Java-Backend (erzeugt Java/Bytecode)
• x10c++ – Compiler mit C++-Backend (für native, leistungsfähige Ausführung)
• runx10 – Startprogramm: verteilt die Ausführung über mehrere places, z. B. runx10 -n 4 Programm (4 places)

Parallelitäts-Konstrukte

finish {
  for (p in Place.places()) {
    async at (p) Console.OUT.println("Hallo von place " + p.id);
  }
}

• async – startet eine neue Aktivität (feinkörnig nebenläufig)
• finish – wartet, bis alle inneren Aktivitäten beendet sind
• at (p) – führt Code auf einem bestimmten place aus; async (p) S ist syntaktischer Zucker für at (p) async S
• atomic – atomare Blöcke für gemeinsame Variablen
• ateach – startet Aktivitäten über alle places einer Verteilung
• Kommunikation über Places (partitionierter globaler Adressraum) statt expliziter Message Passing

Praxis-Tipps

• Kompilieren: x10c++ -o Programm -O Programm.x10, dann runx10 -n 4 Programm
• Für die Datenparallelität gibt es mehrdimensionale verteilte Arrays (Array[T] mit Dist) und Clock-Synchronisation

Verwandte Sprachen: Java-Befehle (X10-Syntax), C/C++-Befehle (C++-Backend), Go-Befehle (Nebenläufigkeit), Xtend-Befehle und Gosu-Befehle. Konzepte: Multikern-Prozessor und Nebenläufigkeit.