🚀 go-pugleaf

RetroBBS NetNews Server

Inspired by RockSolid Light RIP Retro Guy

Article View: comp.specification.z
Article #23

Re: Z and concurrent systems

#23
From: Ismar Neumann Kaufman
Date: Tue, 11 Aug 1992 22:18
49 lines
2851 bytes
 
In article from Aug,11, maria@dain (Maria Brielmann) writes:
 
| I'm looking for some information about Z and specification of concurrent
| systems. I heard some rumours about a special Z dialect for this task. Does
| anybody of you know more details?
 
 
I'm currently working on my MsC dissertation where I propose a way to join
the known advantages of Z and some formal mechanism to specify concurrency.
 
The main idea is to subvert Z semantics in order to have a structured
version of modal action logic as the semantics of a Z+concurrency
specification. In fact, I don't use pure Z, but the object oriented dialect
MooZ, recently cited in this forum and a report of which is available via
FTP.
 
The logic is based on the work of J. Fiadeiro and T. Maibaum and includes
deontic predicates for a very clean way to talk about actions occurrence.
Encapsulation of data is guaranteed by a locality axiom and specifications
are structured by morphisms. Objects communicate through syncronization
when information may be exchanged.
 
Fiadeiro and Maibaum have already proposed a calculus for temporal
reasoning over specifications using deontic predicates. The calculus follow
the structure of the specifications.
 
Syntactically, MooZ needs very little change to incorporate modal action
logic, with the addition of the two deontic predicates (for permission and
obligation) and a "built-in set" called Method, which contains the names of
the class methods where it occurs.
 
In my dissertation (written in portuguese) I show how to translate MooZ
specifications into modal action logic using a denotational style notation.
I'm planning to have, late in September, a technical report about the
language (called MaMooZ), available via ftp. Questions are welcome and if
they are not of general interest, direct them to the email address below.
 
 
+----------------------------------------------------------------+
|                                                                |
| Ismar Neumann Kaufman       Universidade Federal de Pernambuco |
| ink@di.ufpe.br              Departamento de Informatica        |
|                             Recife PE Brazil                   |
|                             phone: +55 81 271 30 52 (lab.)     |
|                                    +55 81 341 08 29 (home)     |
|                                                                |
+----------------------------------------------------------------+
Technical Details
Message-ID: <9208112018.AA25752@di.ufpe.br>
Path: arc1-ca.pugleaf.net!sparky!uunet!mcsun!uknet!ox-prg!ink

Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!sparky!uunet!mcsun!uknet!ox-prg!ink
From: ink@DI.UFPE.BR (Ismar Neumann Kaufman)
Newsgroups: comp.specification.z
Subject: Re: Z and concurrent systems
Message-ID: <9208112018.AA25752@di.ufpe.br>
Date: 11 Aug 92 22:18:54 GMT
Sender: daemon@comlab.ox.ac.uk
Lines: 49
X-Envelope-To: zforum@prg.oxford.ac.uk
X-Mailer: mail-news 2.0.3