Z-Notation bzw. Object-Z-Notation in Latex

[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

[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.

[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

[bloodworks]

Ach du liebe .. .das Paket ist 22 Jahre alt! Nimm lieber mal listings.

texdoc listings

[thenine]

Sorry, ich kann dir nicht folgen, auf was beziehst du dich?

[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)

[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

[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}