This is an archived page and is no longer updated.
Please visit our current pages at https://rvs-bi.de

Werkzeuge für die Betriebssysteme-Übungen

Dirk Henkel

Auf dieser Seite sind einige Informationen über Sprachen und Programme gesammelt, die für die Übungen der Vorlesung Technische Informatik I: Betriebssysteme von Prof. Ladkin von Bedeutung sind. Für die Übungsteilnehmer unentbehrlich sind das Textsatzsystem LaTeX und die Spezifikationssprache TLA+. Die Links zu HTML stehen dagegen nur zum Vergnügen hier. Diese Seite enthält die Abschnitte:

Wer etwas anderes sucht, kann ja mal in meine LinkPage gucken.

LaTeX

LaTeX ist ein vor allem für naturwissenschaftliche und mathematische Anwendungen entwickeltes Textsatzsystem. Wir werden es zum Schreiben von leserlichen Spezifikationen und Beweisen benutzen. Ein Unterschied zu herkömmlichen Textverarbeitungsprogrammen ist, daß sämtliche Formatierungsinformationen als Kommandos (und nicht als Steuerzeichen) in den Text geschrieben werden. LaTeX-Texte können daher auch mit einfachsten Texteditoren geschrieben und zwischen verschiedenen Computersystemen ausgetauscht werden.

Das Programm latex generiert zu einem LaTeX-Text eine sogenannte DVI-Datei. Diese kann dann mit dem Programm xdvi auf dem Bildschirm dargestellt oder mit dem Programm dvips an einen Postscript-Drucker geschickt werden. "DVI" steht für "device independent". Die DVI-Datei enthält den formatierten Text in geräteunabhängiger, aber für Bildschirm- und Druckertreiber leicht verarbeitbarer Form. LaTeX-Text und DVI-Datei verhalten sich zueinander wie Quelltext und compilierter Code eines Programms, latex ist dabei der Compiler. Ein LaTeX-Text ist gewissermaßen ein Programm zum Setzen eines Textes.

Zum Kennenlernen von LaTeX empfehle ich eine kurze, gute und sogar deutschsprachige LaTeX-Einführung. An den .tex-Dateien, aus denen dieses Dokument erzeugt wurde, kann man auch gleich sehen, wie typischer LaTeX-Quelltext aussieht. Wer es genauer wissen will und die englische Sprache nicht scheut, dem sei die etwas längere LaTeX-Introduction empfohlen.

Dies ist nur als Erstinfo gedacht. Wirklich umfangreiche und gut strukturierte LaTeX-Informationen findet man bei LAUB, den LaTeX-Administratoren der Universität Bielefeld.

Von der LaTeX-Datei zum Ausdruck

Um die LaTeX-Datei file.tex zu Papier zu bringen, tut man folgendes: Einige weitere Bearbeitungsmöglichkeiten: Zu allen in diesem Abschnitt erwähnten Programmen gibt es auch Man-Pages. In den Infos zum Drucken im HRZ steht, welche PostScript-Drucker es dort gibt und wie man einen Druck-Account bekommt.

TLA+ und TLA

Ähnlich wie die Euch bekannten Programmiersprachen ist TLA+ eine Sprache zur Beschreibung von Prozessen. In TLA+ werden Prozesse allerdings nicht algorithmisch, sondern logisch beschrieben. Diese Art der Beschreibung ist sehr nützlich für den Beweis, daß ein Prozeß wirklich korrekt abläuft. Eine besondere Stärke von TLA+ liegt in der Möglichkeit, Systeme mit parallel laufenden Prozessen zu beschreiben.

Eine handliche deutschsprachige Einführung in TLA+ (DVI - PostScript) hat Michael Blume geschrieben. Von Leslie Lamport, dem Vater dieser Sprache, gibt es zur Zeit zwei "technical notes" über die Modulstruktur und die Operatoren von TLA+. Mit diesen Veröffentlichungen haben sich einige Modul-Schlüsselwörter geändert. In vielen anderen TLA+-Dokumenten findet man zur Zeit noch die alte Notation.

TLA+ basiert auf dem temporalen Logik-Kalkül TLA (Temporal Logic of Actions). Dazu gibt es (ebenfalls von Leslie Lamport) die Introduction to TLA und den sehr ausführlichen TLA-Report ( LaTeX - DVI - PostScript). Der Report behandelt auch die Anwendung von TLA in Spezifikationen und Beweisen sowie die Unterschiede zwischen TLA und Programmiersprachen. Prof. Ladkin hat ein ebenfalls etwas ausführlicheres Tutorial on TLA Verification geschrieben. Dies ist keine systematische TLA-Einführung, sondern zeigt, wie TLA zum Beweisen von Programmen verwendet wird.
Weitere Texte zu TLA und TLA+ findet man auf der TLA-Homepage von Leslie Lamport und in der Literaturliste der AG RVS.

TLA+ setzen mit LaTeX

Irgendwann in diesem Semester werdet Ihr vor der Aufgabe stehen, mit Hilfe von LaTeX Spezifikationen in TLA+ zu schreiben. Einen ersten Eindruck davon vermittelt am besten ein Beispiel: seht Euch doch mal diese zwei Buffer-Spezifikationen (mit zusätzlichen Funktions-Skizzen) an und vergleicht sie mit dem zugehörigen LaTeX-Quelltext. Größere Beispiele für TLA+-Spezifikationen (und entsprechende Verifikations-Beweise) findet man in den Veröffentlichungen der AG RVS.

Zum Setzen solcher TLA+-Spezifikationen gibt es eine Reihe spezieller LaTeX-Kommandos. Diese gehören nicht zum LaTeX-Standardumfang, sondern sie werden in den Dateien tla.sty, abbrev.sty und pf.sty definiert. Diese TLA-spezifischen Style-Files enthalten ausführliche Kommentare, in denen die dort definierten LaTeX-Kommandos erklärt werden. Zusätzlich werden unter LaTeX2e noch einige Symbol-Definitionen aus der Datei latexsym.sty benötigt (diese gehört zum Standardumfang von LaTeX2e). latexsym.sty und tla.sty werden in einen LaTeX-Text mit dem Kommando 

  \usepackage{latexsym,tla}
eingebunden (siehe Beispiele). tla.sty bindet seinerseits abbrev.sty und pf.sty ein.

GNU Emacs

Dieses Werkzeug gehört nicht zum "Pflichtprogramm" unserer Übungen, aber viele werden wohl damit arbeiten, deshalb werde ich hier auch zum Emacs die Informationen sammeln, die mir über den Weg laufen. Auf jeden Fall gehört hierher ein Verweis auf das GNU Emacs Manual. Neben dieser aktuellen HTML-Version gibt es auch eine etwas ältere im DVI-Format, ein stolzes Buch von 300 Seiten. Das File ist gepackt und kann mit gunzip entpackt werden, falls das der Web-Browser nicht sowieso tut.

Eine Kurzübersicht über die wichtigsten Emacs-Kommandos liefert die GNU Emacs Reference Card. Zum Ausdrucken auf PostScript-Druckern kann man diese mit dvips -tlandscape bearbeiten oder gleich die PostScript-Version an den Drucker schicken. Laßt Euch nicht dadurch verwirren, daß ghostview das Querformat nicht vollständig anzeigt, auf dem Ausdruck ist alles drauf, ich hab's ausprobiert. Wer das dreispaltige Layout zu klein findet oder Probleme mit dem Querformat hat, kann auch am Anfang des Quelltextes ein- oder zweispaltigen Satz einstellen (siehe Kommentar im Quelltext). Achtung: diese Datei muß mit tex, nicht mit latex bearbeitet werden. Und zum Online-Gebrauch ist hier auch noch eine einfache und eine bunte HTML-Version.

Der TeX-Mode von GNU Emacs ersetzt automatisch einen eingegebenen "double quote" durch zwei ``single quotes''. Das ist insbesondere bei der Verwendung des Pakets german unangenehm. Abhilfe schaffen Änderungen in der Datei .emacs in Eurem Home-Verzeichnis. Am einfachsten ist es, wenn Ihr einfach diese Datei nehmt und sie unter dem Namen .emacs in Euer Home-Verzeichnis kopiert. Die entscheidende Zeile dieser Datei ist in diesem Zusammenhang 

(require 'tex-site) .
Sie lädt eine Datei tex-site, die ich nicht näher kenne. Ich vermute, sie checkt die vom editierten LaTeX-File verwendeten Packages. Wenn man eine ganz neue Datei schreibt, findet die störende Ersetzung leider trotzdem statt. Abhilfe: man schreibt den Rahmen: 
\documentclass{...}
\usepackage{...,german}
\begin{document}
\end{document}
speichert die LaTeX-Datei ab und lädt sie neu in den Emacs.

HTML

HTML (HyperText Markup Language) ist wie LaTeX eine Markup-Sprache, d.h. eine Sprache, in der die logische Struktur eines Textes explizit im Text angegeben werden kann. Programme zur Darstellung solcher Texte können mit Hilfe dieser Struktur-Informationen ein geeignetes Layout wählen. Der besondere Schwerpunkt von HTML ist die Möglichkeit, im Text Querverweise auf andere Dateien anzugeben, so daß ein entsprechendes Programm ("Browser") diese Dateien im Internet auffinden und ggf. anzeigen kann. HTML ist die Sprache, in der WorldWideWeb-Seiten wie diese geschrieben werden.

Da HTML nicht so unmittelbar mit der Betriebssysteme-Vorlesung zu tun hat, liste ich hier nur etwas einführende Literatur auf:

Die Einführung von Stefan Münz enthält auch eine strukturierte Kurzreferenz zum Nachschlagen der einzelnen HTML-Befehle.