Seite 1 von 1
Z-Notation bzw. Object-Z-Notation in Latex
Verfasst: Mo 9. Jul 2012, 20:53
von thenine
Hallo,
ich schreibe meine Diplomarbeit mit Latex und benutze die Spezifikationssprachen Z und Object-Z. Laut ISO Standard (ISO 13568) ist es möglich IF-Anweisungen in Z zu notieren (Befehl: \IF \THEN). In meiner Object-Z-Spezifikation erkennt Latex diese Keywords nicht. Eingebunden habe ich das package oz.
Hat jemand damit Erfahrungen?
thx, Janine
Verfasst: Mo 9. Jul 2012, 22:09
von bloodworks
Hä? du bindest Source Code ein ? Also ich versteh nur Bahnhof. Wie wärs denn mit einem Minimalbeispiel [2]. Dann wüsste jeder sofort bescheid.
Verfasst: Di 10. Jul 2012, 09:19
von thenine
Wie gewünscht das Minimalbsp
\documentclass{article}
\usepackage[a4paper]{geometry}
%\usepackage{latexsym} % Fuer recht seltene Zeichen
\usepackage{amsfonts} % Mathe-Schriften
\usepackage{amssymb} % Symbole
\usepackage{amsmath}
\usepackage{graphicx}
\usepackage{caption}
\usepackage{oz} % Object-Z
\begin{document}
\begin{figure}[h]
\centering
\begin{class}{Set}
\
\begin{op}{Add}
\Delta (s, count)\\
x?: \nat
\ST
%\if %<--------------------------------------hier
x? \notin s \\
s' = s \cup \left\{x?\right\} \\
count' = count + 1
%\fi %<--------------------------------------hier
\end{op}
\end{class}
\caption{\text{Beispiel einer Object-Z Spezifikation}}
\label{fig:bild100}
\end{figure}
\end{document}
Wenn ich den \if-Befehl einbinde, kommt
! Incomplete \if; all text was ignored after line 21.
<inserted text>
\fi
Wenn ich den \fi-Befehl einbinde, verschwindet ein Teil meiner Spezifikation.
Janine
Verfasst: Di 10. Jul 2012, 09:42
von bloodworks
Ach du liebe .. .das Paket ist 22 Jahre alt! Nimm lieber mal listings.
Verfasst: Di 10. Jul 2012, 09:59
von thenine
Sorry, ich kann dir nicht folgen, auf was beziehst du dich?
Verfasst: Di 10. Jul 2012, 10:09
von bloodworks
Auf das Paket listings. Das ist sozusagen Standard beim Einbinden von Quelltext. Du kannst ja mal schauen ob dir das hilft.
Dass es bei if und fi Fehler gibt wundert mich tatsächlich auch nicht. Das sind core Befehle, selbst wenn man die sauber umdefinieren kann wäre es doch ziehmlich pervers.
Abgesehen davon macht das das Paket auch nicht. In der ganzen Doku steht kein einziges mal was von \if. (Es gibt \iff)
Verfasst: Di 10. Jul 2012, 10:39
von thenine
Object-Z ist keine Programmiersprache sondern eine Spezifikationssprache, sprich eine Ebene oben drüber. Es ist ähnlich einer Beschreibungssprache wie z.B. UML. Das package oz stellt die Strukturen bereit um eine Object-Z-Spezifikation zu notieren (einfach mal die Tex-Datei ausführen). So eine Spezifikation kann dann in eine beliebige Programmiersprache übersetzt werden.
In einem Paper habe ich eine Object-Z-Spezifikation mit IF und THEN gesehen und wollte das auch in meine Spezifikation einbinden.
Da Object-Z auf Z aufbaut und es dort die Befehle \IF \THEN \ELSE (ich habe noch einmal nachgeschlagen, \if ist falsch ) gibt. Bin ich davon ausgegangen, dass das package oz diese auch kennt. Anscheinend sind diese aber nicht im package oz definiert. Eine Möglichkeit an der ich gerade arbeite ist das package für z ebenfalls noch ein zubinden, aber ich glaube das wird nicht funktionieren.
Janine
Verfasst: Di 10. Jul 2012, 12:17
von bloodworks
Also wie gesagt das Paket ist uralt. Warum machst du das nicht einfach mit dem Mathe Modus?
\documentclass{article}
\usepackage{amsfonts} % Mathe-Schriften
\usepackage{amssymb} % Symbole
\usepackage{amsmath}
\usepackage{dsfont}
\begin{document}
\begin{figure}[h]
\centering
\begin{equation*}
\begin{array}{|l}
\Delta (s, count)\\
x?: \mathds{N} \\\hline
\text{\textbackslash if} \\ %<--------------------------------------hier
x? \notin s \\
s' = s \cup \left\{x?\right\} \\
count' = count + 1\\
\text{\textbackslash fi} %<--------------------------------------hier
\end{array}
\end{equation*}
\caption{\text{Beispiel einer Object-Z Spezifikation}}
\label{fig:bild100}
\end{figure}
\end{document}