[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):