Isabelle ist ein generischer, interaktiver Theorembeweiser (Proof Assistant), mit dem sich mathematische Sätze und Programmeigenschaften maschinell überprüfen lassen. Entwickelt wurde er ab Mitte der 1980er-Jahre von Lawrence C. Paulson an der University of Cambridge, aufbauend auf Robin Milners Edinburgh-LCF-System; der Name geht auf Gérard Huets Tochter zurück. Isabelle ist in Standard ML geschrieben und hat mit Isabelle/HOL (Higher-Order Logic) eine Hauptobjektlogik, in der die meisten formalen Verifikationen stattfinden.

Strukturierte Beweise mit Isar

Seit der Version von 1999 bietet Isabelle mit Isar eine strukturierte Beweissprache, die Beweise lesbar und nachvollziehbar macht:

lemma add_comm: "a + b = b + a"
proof -
  show ?thesis by (induct a) simp_all
qed

Klassische Beweisbefehle im apply-Stil: apply (rule r), apply auto, apply simp, apply (blast intro: …), abgeschlossen mit done.

Automatisierung

• sledgehammer ruft externe automatische Beweiser (E, Vampire, Z3, Spass) auf und rekonstruiert gefundene Beweise in Isabelle — das Herzstück für produktives Arbeiten.
• nitpick und quickcheck suchen Gegenbeispiele beziehungsweise Testinstanzen zu Behauptungen.
• find_theorems und find_consts durchsuchen die vorhandene Wissensbasis; value und term evaluieren Ausdrücke.

Werkzeuge

isabelle build -b HOL
isabelle jedit -l HOL theory.thy
isabelle process -T theory

Das Archive of Formal Proofs (AFP) sammelt hunderte verifizierte Theorien. Berühmte Projekte auf Isabelle-Basis: der seL4-Mikrokernel und der CompCert-C-Compiler.

Verwandte Beweisassistenten sind Coq und Lean. Wer das Verhalten nebenläufiger Systeme als ausführbares Modell prüfen will, nutzt dafür TLA+; wer Prozessmodelle maschinell prüfen will, nutzt Promela mit dem Model Checker SPIN; wer automatisch nach Gegenbeispielen sucht, den Alloy Analyzer.

tcsh (TENEX C Shell) ist die erweiterte Version der C-Shell, die Ken Greer Ende der 1970er Jahre an der Carnegie Mellon University entwickelte. Das t steht für TENEX, ein Betriebssystem, dessen Kommandozeilen-Features als Vorbild dienten. tcsh ist vollständig abwärtskompatibel zu csh und hat es auf vielen Systemen als Standard-Shell abgelöst (z. B. lange Zeit auf FreeBSD).

Erste Schritte

set prompt = "%m:%c3> "   # Host:Verzeichnis als Prompt
set autolist                  # Tab-Vervollständigung
set correct = all             # Rechtschreibkorrektur
Ctrl-R                        # rückwärts in der History suchen

Kernkonzepte

• Kommandozeilen-Editing: vi- oder emacs-Modi, History-Suche per Ctrl-R
• Programmierbare Vervollständigung: set autolist, set filec, complete für eigene Vervollständigungsregeln
• Rechtschreibkorrektur: set correct korrigiert Befehle und Dateinamen automatisch
• Prompt-Erweiterungen: %n (User), %m (Host), %~ (Pfad), %# (Root-Marker)
• watch: Benachrichtigung bei Logins anderer User
• Einzigartige History-Formen: z. B. ^alt^neu zum Ersetzen im letzten Kommando

Einordnung

tcsh kombiniert C-Shell-Syntax mit Komfort, der erst Jahre später in andere Shells einzog. Moderne Alternativen mit ähnlichem Bedienkomfort sind Fish, Zsh oder Nushell.

ksh (Korn-Shell) ist eine Unix-Shell von David Korn bei den AT&T Bell Laboratories, vorgestellt 1983. Sie vereint die Stärken der Bourne-Shell mit Komfort-Features der C-Shell und ist weitgehend POSIX-kompatibel. Die wichtigste Variante ist ksh93, die bis etwa 2012 von Korn und Glenn Fowler weiterentwickelt wurde.

Erste Schritte

ksh -c 'print "Hallo Welt"'
history
alias ll='ls -l'
typeset -i zahl=5

Kernkonzepte

• print: Ausgabe (Alternative zu echo)
• typeset: Variablen und Attribute setzen (z. B. typeset -i für Integer-Arithmetik)
• [[ ]]: erweiterte Bedingungen mit Mustergleich
• (( )): arithmetische Ausdrücke, z. B. (( sum = a + b ))
• select: interaktive Auswahlmenüs in Skripten
• function: Funktionen definieren, whence: Befehlspfad ermitteln
• Coprozesse: |& für bidirektionale Kommunikation mit Hintergrundprozessen

Kommandozeilen-Editing

ksh bringt von Haus aus bearbeitbare History mit — im vi- oder emacs-Modus (set -o vi bzw. set -o emacs). Das war Mitte der 1980er Jahre ein Alleinstellungsmerkmal.

Praxis

ksh war lange die Standard-Login-Shell auf AIX und Solaris und ist bis heute POSIX-konforme Wahl für robuste Administrations-Skripte. Wer eine modernere, komfortablere interaktive Shell sucht, findet sie in der Bash oder Zsh. Die Verwandtschaft zeigt sich auch bei csh und tcsh — sie stammen aus derselben Shell-Epoche.

csh (C Shell) wurde 1978 von Bill Joy an der University of California, Berkeley, entwickelt und mit BSD Unix verbreitet. Ihre Syntax lehnt sich an die Programmiersprache C an. csh führte mehrere Komfort-Features ein, die heute selbstverständlich sind: History, Aliase und Job Control.

Erste Schritte

setenv PATH "$PATH:/usr/local/bin"
alias ll 'ls -l'
history
!!            # letztes Kommando wiederholen
!$            # letztes Argument wiederholen

Kernkonzepte

• setenv / set: Umgebungs- bzw. lokale Variablen (set var = wert, Zugriff über $var)
• alias: Kurzbefehle definieren
• history: Liste der letzten Kommandos, Wiederholung über !-Kürzel
• Job Control: jobs, fg, bg, %1 für Hintergrund-/Vordergrundprozesse
• switch/case: C-artige Verzweigung in Skripten
• foreach: Schleife über Listen

Einordnung

csh war als interaktive Shell sehr beliebt, ihre Skriptsprache gilt jedoch als fehleranfällig und ist nicht POSIX-konform — für Skripte empfiehlt sich bis heute die Bourne-Shell-Familie wie Bash. Die C-Shell-Linie lebt in tcsh weiter, das als direkter Nachfolger fast überall csh ersetzt hat.