Stack Overflow
Stack Overflow

Questions tagged [z-notation]

Use this tag with the Z notation /ˈzɛd/ which is a formal specification language used for describing and modelling computing systems.

33 questions
15
votes
6 answers

Known "Z notation" applications?

I was just remembering back my university classes and was wondering to know if anyone out here even used the "Z notation" in a professional environment. I honestly must say that it was the single most boring class that I have ever attended in my…
Amadeus45
  • 1,228
  • 2
  • 17
  • 28
7
votes
3 answers

Z specifications in LaTeX

Is there any package for LaTeX which will support writing Z specifications? I am interested in both horizontal and vertical formats for schemas.
Gabriel Ščerbák
  • 18,240
  • 8
  • 37
  • 52
7
votes
2 answers

Zed Notation in LyX

Is it possible to create Zed Notation schemes in LyX? How can it be done?
Amir Rachum
  • 76,817
  • 74
  • 166
  • 248
3
votes
1 answer

How to prove (p^q) ^ ( q -> r ) <-> r using Z- notation?

I am trying to prove logical expressions using Z-notations. But, I am new to the Z language. Please help me to prove the above logical expression.
Sajith Madusanka
  • 33
  • 3
3
votes
1 answer

Z Notation: Representation of a 2D array

I'm a complete beginner at the Z notation. I need to represent a graph type in Z. The idea I have is to use an incidence matrix so that I can traverse freely between nodes and edges with ease. The only problem is, I don't know how to specify the…
MaXim
  • 63
  • 1
  • 5
2
votes
2 answers

Formatting of Strings in Latex in whitespace insensitive environment / Z-Notation Schema

I'm using latex to model a few functions using Z-Notation, however, I'm having issues showing a string for output. In this reduced example code, the text in the quotes has a different formatting from what I would expect. What can I use to keep the…
JosephTLyons
  • 2,075
  • 16
  • 39
2
votes
1 answer

How to represent unique attribute in Z-notation without quantifiers?

Full disclosure, this is for a university course. I don't expect an answer outright, but help would be appreciated. I need to model an Item entity using Z-notation. This is the description: Item: Every item has a name and a unique ID which can be…
S. Fenoll
  • 23
  • 1
  • 4
2
votes
1 answer

Zed specification: Promotion and applying an operation more than one schema

I have an Array schema that keeps track of sequence of Data schemas. Using promotion, I am able to promote Increment operation to use with Array. ArrayIncrement only increments one data inside Array. How do I make it such that it increments every…
iH8WorkingWith.NetGraphics
  • 418
  • 1
  • 6
  • 16
2
votes
1 answer

how to formalize Uml

Is there a way to convert(formalize) UML to Z notation? what I mean is that is there any way to re-write UML requirements to a formal language like z? sorry for my bad English, my native language is not English. thank you.
Ileden
  • 25
  • 1
  • 5
1
vote
1 answer

Isabelle/HOL with HOL-Z and ZETA

I have seen some papers that describe how to use the Z notation with Isabelle/HOL using the tools HOL-Z and ZETA. I was not able to find these tools, have they ever been published? Are there other ways to use Isabelle with the Z notation?
dordow
  • 115
  • 6
1
vote
1 answer

Why is there a difference of one in down function of Z notation for the solution to 8 Queen problem?

I was reading the book titled "The Way of Z: Practical Programming with Formal Methods by Jonathan Jacky" and in chapter 18 (8 Queen problem), the author provided a Z notation based formal solution to the famous 8 queen problem. He tried to solve…
Muhammad Zohaib Nawaz
  • 53
  • 7
1
vote
2 answers

Z notation: How to write operation schema that may add one or more tuples to a relation

I'm writing an operation schema in Z. This operation AssignValue maps a property to one or more values. One property may be linked to one or more values, and one value may be linked to one or more properties, forming a many-to-many relation, R ⊆…
snow
  • 47
  • 3
1
vote
2 answers

How to do inclusion of schema in other schema using Z language

I am writing a formal specification for my model using z-notation of Z-language. I am stuck and don't know how to include one schema in another schema and creates its variables in other schemas. Any guidance and help would be appreciated. Thanks.
Yasir Darr
  • 43
  • 6
1
vote
0 answers

Interpretation of Partial Functions from Z to Isabelle/HOL

I am trying to write a predicate such that, "if a certain constant is true"(in this case if 'sec=ok') then the predicate will evaluate to False, because I've written an expression in the consequent of that particular implication that contradicts…
user3896306
  • 11
  • 1
1
vote
1 answer

need a definition in Isabelle to show that two partial functions never produce the same output

I'm using the mathematical toolkit in HOL-Z to discharge some Isabelle predicates. specifically I'm using the partial function definition to define some of the relations in a Z specification that I'm writing, where I convert the schema's to…
Shiyam
  • 71
  • 5
1
2 3