[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> 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
Reference(s):