----- Mensaje reenviado por Michael Jackson <jacksonma@acm.org> -----
Date: Sat, 22 Mar 2003 12:06:22 +0000
From: Michael Jackson <jacksonma@acm.org>
Reply-To: Michael Jackson <jacksonma@acm.org>
Subject: Re: Question regarding designations
To: Maximiliano Cristia <mcristia@fceia.unr.edu.ar>

Dear Maximiliano,

Thank you for your email message, and also for your interest
in my work.

There is no restriction on the formal expressions or terms used
to denote phenomena. However, it is a good general rule not to
embed assertions either in definitions or in designations (beyond
the implicit assertion in any designation that the phenomena can
be reliably recognsied). It would be contrary to this rule to write
a designation

   t is the temperature of patient p <=>
                      (p,t) in PatientTemp: Patient -> Temp

because it embodies the assertion that the relation "Patient <->
Temp" is a function. It also embodies the assertion that the domain
of PatientTemp is the set of Patients, and its range is the set of
Temps. It would be better to separate out the assertions, and write
the designation as

   t is the temperature of patient p <=> (p,t) in PatientTemp

with the separate assertions

   (p,t) in PatientTemp => (p in Patient) /\ (t in Temp) /\
                                       forAll u . (p,u) => u = t

and so on.

I hope this is helpful.

Best wishes,

-- Michael Jackson



Maximiliano Cristia wrote:

> Dear Michael Jackson,
>
> My name is Maximiliano Cristia. I'm a Software Engineering teacher at
> Rosario University, Argentina.
>
> This year, I decided to include your (and Zave's) reference model and
> approach to software requirements and specificacions in the Software
> Engineering course. In this course I also include various formal
> specification languages such as Z, Larch and TLA.
>
> The question is: should designations necessarly be predicates or proper
> names for individuals only? I'm asking this question because designations
> must be used in requirements, domain knowledge and specifications
> descriptions and if I write these descriptions, say, with Larch some of
> its power will be lost (it would be unnecessarly restrictive to use many
> functions into Bool just because designations are predicates).
>
> For example, say I have the following designation
>
> t is the temperature of patient p <=> PatientTemp(p,t)
>
> so if I want to specify with Larch I must define a trait with a function
> laike this
>
> PatientTemp: Patient, Temperature -> Bool
>
> when it could be more "natural" to write
>
> PatientTemp: Patient -> Temperature
>
> (if domain knowledge assures that PatientTemp is indeed a function).
>
> What should I tell to my students? What should I do? Can I generalize the
> "type" of designations to functions? Should I use a new name, say PatTemp,
> to denote PatientTemp in the Larch specificaction and include a predicate
> relating both of them?
>
> I hope you find the time to help me, if not I understand and thank you
> very much any way.
>
> (I forget to say that your model is what I was looking for in last two
> years)
>
> Sincerely,
>  Maximiliano Cristia

----- Fin del Mensaje reenviado -----