[Prev][Next][Index]
Re: Partial Functions and Logics
>>>>> "CHALIN" == CHALIN patrice <chalin@cs.concordia.ca> writes:
In article <4109ub$kja@newsflash.concordia.ca> chalin@cs.concordia.ca (CHALIN patrice) writes:
CHALIN> Here is the abstract of [Jon95]
CHALIN> One approach to handling partial functions when
CHALIN> specifying and reasoning about programs is to say that
CHALIN> application outside their domain yields an indeterminate
CHALIN> element of their range. This paper puts forward a counter
CHALIN> example which suggests that this approach might be
CHALIN> problematic in a specification language.
CHALIN> I fail to see the problem that the paper is meant to point
CHALIN> out (so I hope that someone can help me out). In response
CHALIN> to [Jon95], I make some remarks concerning Larch and Z
CHALIN> [Spi89] below.
CHALIN> Z
CHALIN> Consider a Z version of the first example used in
CHALIN> [Jon95].
I'm happy with the changed example.
CHALIN> [Unit] ...
CHALIN> From this specification (let us call it SPEC1) we can
CHALIN> prove that
CHALIN> forall i: ZZ @ f i = u
Really? That is precisely my point - we are discussing specification
languages - I just can't believe that the writer of the definition of
f would expect that.
Of course, in this example it is easy to see what is going on - but in
more subtle cases I think that the least fixed point interpretation of
functions is very intuitive and doing anything that moves away from it
should be done with great caution.
The point of my original note (see the "equations" about fact(orial))
was this worry about the meaning of functions. Saying that all terms
denote, pushes through recursive definitions to give some odd results.
CHALIN> ...
CHALIN> By the ``customary Z stylistic guidelines'', the SPEC1
CHALIN> definition of f would be considered incomplete. Spivey
CHALIN> writes, ``Partial functions may be defined by giving their
CHALIN> domain and their value for each argument in the domain'';
CHALIN> by doing so we completely determine the partial function
CHALIN> being defined [Spi89, p.43,]. Thus, in general, partial
CHALIN> functions can be defined using recursive equations only if
CHALIN> their domains have been fixed (outside of the recursive
CHALIN> equation)...
Where do these ``customary Z stylistic guidelines'' fit into a formal
semantics of a specification language?
CHALIN> ... ... ... ... ... ... ... ...
CHALIN> In the light of what I stated above, it would not seem
CHALIN> necessary that `Z' fix denotations for its recursively
CHALIN> defined functions since this is not the kind of
CHALIN> interpretation that is applied to Z specifications.
Hmmm!
cliff jones
Follow-Up(s):
Reference(s):