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> Larch

    Chalin> As has already been stated in the postings to
    Chalin> comp.specification.larch, in the logic underlying the
    Chalin> Larch Shared Language (let us refer to this logic as LL),
    Chalin> all function are total, hence [Jon95] does not directly
    Chalin> concern LL.

If you mean that -as in Boyer/Moore- the user must prove (e.g. with a
measure) that all functions are total over their domains (as given in
their type), then I concede that the specific point that I was making
does not apply.

The above was not the situation in LL when Jim Horning tried to push
an example of mine through LP.

    Chalin>  ``The originators of Larch [GH93] are prepared to
    Chalin> restrict types to having more than one value.'' [Jon95,
    Chalin> p.66,].

The same goes for this point - I'm sorry that I stated the Larch
position without checking it hadn't changed.

BTW I don't like the requirement to prove all functions total - but
that is a different issue.

    Chalin> Z

I'll tackle this in a separate reply

cliff jones