Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Path: utzoo!utcs!mnetor!lsuc!dave
From: dave@lsuc.UUCP
Newsgroups: net.lang.prolog
Subject: Re: "assert" considered harmful?
Message-ID: <1245@lsuc.UUCP>
Date: Thu, 12-Jun-86 01:16:04 EDT
Article-I.D.: lsuc.1245
Posted: Thu Jun 12 01:16:04 1986
Date-Received: Thu, 12-Jun-86 03:29:08 EDT
References: <1754@utai.UUCP> <269@ubc-cs.UUCP>
Reply-To: dave@lsuc.UUCP (David Sherman)
Organization: Law Society of Upper Canada, Toronto
Lines: 45
Summary: proving applications correct - important?

(I must say this interaction with knowledgeable people on the net, from
the point of view of someone merely trying to design an application, is
fascinating. Thanks to everyone who's contributed so far.)

In article <269@ubc-cs.UUCP> andrews@ubc-cs.UUCP (Jamie Andrews) writes:
>
>     It should be of little concern to applications programmers that
>these features destroy the declarative reading of the program, unless they
>have to prove to their bosses that their applications are rigorously
>correct. 

Interesting issue. What happens if I succeed in designing a tool
which can be used for corporate tax planning, and I want to make
it a commercial product? Should it be "provably" correct before
lawyers use it?

What I've done with the problem, incidentally, is do some
initial "setup" work which analyses all of the relationships
stated in the facts and asserts the things it determines to
be true. So, for example, I have the definition of control
(>50% of voting power, etc.) in a predicate called controls_rule,
and the predicate "controls" either exists as a stated fact (set
up by the user) or is asserted at setup time. Thereafter all tests
refer simply to "controls". Same thing for "related_rule" and
"related", which incidentally solves the thorny problem of
circularity caused by definitions which define related
taxpayers in terms of other related taxpayers - I simply call
the setup routine enough times to make sure all derivative
relationships are asserted. (Hope that isn't too obscure.)

Of course, the thing will get a lot more difficult when I
properly implement time, which is crucial to the system. But
I think it's still reasonable to determine what each time
interval is that's relevant, and make the assertions relative
to those time intervals.

As long as I limit my assertions by restricting the time interval,
then I don't really have to worry about the difference between
"assert" and "assume" which was mentioned by Anand Rao, do I?

Dave Sherman
The Law Society of Upper Canada
Toronto
-- 
{ ihnp4!utzoo  pesnta  utcs  hcr  decvax!utcsri  } !lsuc!dave