ProZ - Revision history

David Geleßus: Fix article PDF link

2021-02-03T17:06:59Z

Fix article PDF link

← Older revision		Revision as of 17:06, 3 February 2021
Line 1:		Line 1:
	[[Category:User Manual]]__NOTOC__		[[Category:User Manual]]__NOTOC__
	ProZ is a extension of the ProB animator and model checker to support Z specifications. It uses the [http://spivey.oriel.ox.ac.uk/mike/fuzz Fuzz Type Checker] by Mike Spivey for extracting the formal specification from a LaTeX file. On the website you can also find documentation about the syntax of Z specifications. The [~~http~~://~~www~~.~~stups.uni-duesseldorf~~.de/w/~~Special:Publication~~/proz07 iFM'07 article on ProZ] contains more details about the implementation.		ProZ is a extension of the ProB animator and model checker to support Z specifications. It uses the [http://spivey.oriel.ox.ac.uk/mike/fuzz Fuzz Type Checker] by Mike Spivey for extracting the formal specification from a LaTeX file. On the website you can also find documentation about the syntax of Z specifications. The [https://www3.hhu.de/stups/downloads/pdf/proz07.pdf iFM'07 article on ProZ] contains more details about the implementation.

	= Preferences =		= Preferences =

Michael Leuschel: /* Summary of Supported Operators */

2015-09-16T15:56:13Z

Summary of Supported Operators

← Older revision		Revision as of 15:56, 16 September 2015
Line 174:		Line 174:
	\lnot P negation		\lnot P negation

			Quantifiers:
			------------
			\forall x:T \| P @ Q universal quantification (P => Q)
			\exists x:T \| P @ Q existential quantification (P & Q)
			\exists_1 x:T \| P @ Q exactly one existential quantification

	Sets:		Sets:
	-----		-----

Michael Leuschel: /* Summary of Supported Operators */

2015-09-16T15:50:30Z

Summary of Supported Operators

← Older revision		Revision as of 15:50, 16 September 2015
Line 271:		Line 271:
	items E bag of items in a sequence		items E bag of items in a sequence
	n \otimes B bag scaling		n \otimes B bag scaling

			Other:
			-----------
			\IF P \THEN E \ELSE F if-then-else expression
			(\LET x == E @ F) Let-expression
	</pre>		</pre>

Michael Leuschel: /* Known Limitations */

2015-09-16T15:47:31Z

Known Limitations

← Older revision		Revision as of 15:47, 16 September 2015
Line 162:		Line 162:
	** probably other?		** probably other?
	* The error messages are not very helpful yet.		* The error messages are not very helpful yet.

			== Summary of Supported Operators ==

			<pre>
			Logical predicates:
			-------------------
			P \land Q conjunction
			P \lor Q disjunction
			P \implies Q implication
			P \iff Q equivalence
			\lnot P negation

			Sets:
			-----
			\emptyset empty set
			\{E,F\} set extension
			\{~x:S \| P~\} set comprehension
			E \in S element of
			E \notin S not element of
			S \cup T union
			S \cap T intersection
			S \setminus T set difference
			\power S power set
			\# S cardinality
			S \subseteq T subset predicate
			S \subset T strict subset
			\bigcup A generalized union of sets of sets
			\bigcap A generalized intersection of sets of sets

			Pairs:
			------
			E \mapsto F pair
			S \cross T Cartesian product
			first E first part of pair
			second E second part of pair

			Numbers:
			--------
			\nat Natural numbers
			\num Integers
			\nat_1 Positive natural numbers
			m < n less
			m \leq n less equal
			m > n greater
			m \geq n greater equal
			m + n addition
			m - n difference
			m * n multiplication
			m \div n division
			m \mod n modulo**
			m \upto n m..n
			min S minimum of a set
			max S maximum of a set
			succ n successor of a number

			**: modulo of negative numbers not supported

			Functions:
			----------
			S \rel T relations
			S \pfun T partial functions from S to T
			S \fun T total functions from S to T
			S \pinj T partial injections from S to T
			S \inj T total injections from S to T
			S \bij T total bijections from S to T
			\dom R domain
			\ran R range
			\id S identity relation over S
			S \dres R domain restriction
			S \ndres R domain anti-restriction
			R \rres S range restriction
			R \nrres S range anti-restriction
			R \oplus Q overriding
			R \plus transitive closure

			Sequences:
			----------
			\langle E,... \rangle explicit sequence
			\seq S sequences over S
			\seq_1 S non-empty sequences
			\iseq S injective sequences over S
			rev E reverse a sequence
			head E first element of a sequence
			last E last element of a sequence
			tail E sequence with first element removed
			front E all but the last element
			E \cat F concatenation of two sequences
			\dcat ss concatenation of sequences of sequences
			E \filter F subsequence of elements of sequence E contained in set F
			E \extract F extract subsequence from F with indexes in set E
			squash F compaction
			E \prefix F sequence E is a prefix of F
			E \suffix F sequence E is a suffix of F
			E \inseq F E is a sequence occuring in the middle of F (segment relation)
			\disjoint E family of sets E is disjoint
			E \partition F family of sets E is a partition of set F

			Bags:
			----------
			\bag S bags over S
			\lbag E,... \rbag explicit bag
			count B E count of occurences of E in bag B
			B \bcount E infix version of count
			E \inbag B bag membership
			B \subbageq C sub-bag relation
			B \uplus C bag union
			B \uminus C bag difference
			items E bag of items in a sequence
			n \otimes B bag scaling
			</pre>

Michael Leuschel: /* Graphical animation */

2014-06-27T05:53:05Z

Graphical animation

← Older revision		Revision as of 05:53, 27 June 2014
Line 118:		Line 118:


	[[File:ProZ_jars.png]]		[[File:ProZ_jars.png\|600px\|center]]

	== Special constructs ==		== Special constructs ==

Michael Leuschel: /* Graphical animation */

2014-06-27T05:49:12Z

Graphical animation

← Older revision		Revision as of 05:49, 27 June 2014
Line 95:		Line 95:
	The type used for images must be an enumerated set where the names of the elements denote their file names (without the suffix .gif).		The type used for images must be an enumerated set where the names of the elements denote their file names (without the suffix .gif).

	Please see the specification '''jars.tex''' which is bundled with the ProB Tcl/Tk version for [[Download]] (inside the examples/Z/GraphicalAnimation/ directory). This is the ~~schema~~ that defines the animation function (actually it is a pair of animation functions: the default function over which the other function is overlaid):		Please see the specification '''jars.tex''' which is bundled with the ProB Tcl/Tk version for [[Download]] (inside the examples/Z/GraphicalAnimation/ directory). This is the part of the specification that defines the animation function (actually it defines a pair of animation functions: the default function over which the other function is overlaid; see [[Graphical_Visualization]] for more details):
			We declare a type for the used images, the names of the elements refer to the file names of the GIF files.
			\begin{zed}
			Images ::= Filled \| Empty \| Void
			\end{zed}
			The animation consists of a grid of images that is updated in each new state.
			The $animation\_function$ maps a coordinate to an image where $(1\mapsto 1)$ is the upper-left corner.
	\begin{schema}{ProZ\_Settings}		\begin{schema}{ProZ\_Settings}
	Level \\		Level \\
Line 109:		Line 114:
	\t2 global\_maximum+1-l\mapsto c\} \cross \{Filled\})		\t2 global\_maximum+1-l\mapsto c\} \cross \{Filled\})
	\end{schema}		\end{schema}

			Here is how the animation of the specification should look like:


			[[File:ProZ_jars.png]]

	== Special constructs ==		== Special constructs ==

Michael Leuschel at 05:46, 27 June 2014

2014-06-27T05:46:31Z

@@ Line 95: / Line 95: @@
 The type used for images must be an enumerated set where the names of the elements denote their file names (without the suffix .gif).
-Please see the specification '''jars.tex''' in the examples section.
+Please see the specification '''jars.tex''' which is bundled with the ProB Tcl/Tk version for [[Download]] (inside the examples/Z/GraphicalAnimation/ directory). This is the schema that defines the animation function (actually it is a pair of animation functions: the default function over which the other function is overlaid):
 == Special constructs ==

Michael Leuschel at 15:44, 23 February 2012

2012-02-23T15:44:47Z

← Older revision		Revision as of 15:44, 23 February 2012
Line 1:		Line 1:
	[[Category:User Manual]]__NOTOC__		[[Category:User Manual]]__NOTOC__
	ProZ is a extension of the ProB animator and model checker to support Z specifications. It uses the [http://spivey.oriel.ox.ac.uk/mike/fuzz Fuzz Type Checker] by Mike Spivey for extracting the formal specification from a LaTeX file. On the website you can also find documentation about the syntax of Z specifications.		ProZ is a extension of the ProB animator and model checker to support Z specifications. It uses the [http://spivey.oriel.ox.ac.uk/mike/fuzz Fuzz Type Checker] by Mike Spivey for extracting the formal specification from a LaTeX file. On the website you can also find documentation about the syntax of Z specifications. The [http://www.stups.uni-duesseldorf.de/w/Special:Publication/proz07 iFM'07 article on ProZ] contains more details about the implementation.

	= Preferences =		= Preferences =

Daniel Plagge at 10:06, 23 August 2011

2011-08-23T10:06:25Z

← Older revision		Revision as of 10:06, 23 August 2011
Line 83:		Line 83:
	ProZ tries to identify components. So, it is recommended to use schema definitions instead of abbreviation definitions (\defs instead of ==) when defining state, initialization, operations, etc.		ProZ tries to identify components. So, it is recommended to use schema definitions instead of abbreviation definitions (\defs instead of ==) when defining state, initialization, operations, etc.

			== Graphical animation ==

			('''Please note that this functionality is part of the next version. If you want to use graphical animation, please download a version from the [[Download#Nightly Build\|Nightly build]].''')

			Analogous to the graphical animation for B specifications, you can define a function that maps a coordinate to an image.
			Then ProZ will display the grid of images while animating the specification.

			To use this feature, add a schema '''Proz_Settings''' that contains a variable
			'''animation\_function'''. The animation function should map a coordinate to an image. A coordinate is a pair of numbers or given sets.

			The type used for images must be an enumerated set where the names of the elements denote their file names (without the suffix .gif).

			Please see the specification '''jars.tex''' in the examples section.

	== Special constructs ==		== Special constructs ==

Daniel Plagge: /* Known Limitations */

2011-05-11T07:01:38Z

Known Limitations

← Older revision		Revision as of 07:01, 11 May 2011
Line 123:		Line 123:
	== Known Limitations ==		== Known Limitations ==
	* Generic definitions are not supported yet.		* Generic definitions are not supported yet.
	* Bags are not supported yet.
	* Miscellaneous unsupported constructs		* Miscellaneous unsupported constructs
	** disjoint
	** partition
	** reflexive-transitive closure		** reflexive-transitive closure
	** probably other?		** probably other?
	* The error messages are not very helpful yet.		* The error messages are not very helpful yet.