From: heym@cis.ohio-state.edu (Wayne Heym)
Subject: Re: Assertions for programming design
Followup-To: comp.lang.eiffel
Summary: Proofs of correctness, as well as assertion-checking and testing, are valuable.
Originator: heym@mum.cis.ohio-state.edu
Keywords: assertions, proofs of correctness, specification, formal methods
Organization: The Ohio State University, Department of Computer and Information Science
Date: Wed, 15 Apr 1992 16:01:24 GMT

In article <1992Apr6.143103.6335@merlin.hgc.edu> jcm@hgc.edu (James McKim) writes:
>In article <1992Apr3.104752.17417@sun.pcl.ac.uk> priestm@sun.pcl.ac.uk (Mark Priestley) writes:
>>In article <1992Apr1.143335.27588@merlin.hgc.edu> jcm@hgc.edu (James McKim) writes:
>
>[Discussion of earlier stack "specification" deleted]
>

[I have deleted Jim's paragraph indicating several things that were
indeed specified in his partial, run-time-checkable specification.]

>>Very true. There seems to be a conflict in this example between the desire to
>>use assertions as specifications and the desire to generate run-time checks
>>from assertions. To do the latter you need a simple Boolean expression that can
>>be evaluated at a single fixed point in the code, eg at the end of a routine,
>>but this is not a sufficiently powerful mechanism to specify the interaction
>>between two routines, as in this case.
>
>Well said!
> 

Jim and Mark have agreed that there is a conflict between the ability
to perform run-time checking of assertions and the ability to use
those assertions to fully specify program behavior.  I also agree.
Jim also said in this article that it is better to give a partial
specification than none at all.  This position seems reasonable.  It
is clear that Jim believes that run-time checking of assertions is
valuable; checking is better than not checking.  So far, so good.
Let's use run-time checking to our advantage.  But let's not assume
that we must stop there.

We can take advantage of existing model-based or axiom-based
specification languages to provide a complete, abstract specification
of program behavior.  And we can encourage efforts to establish a
combination of (1) programming language, (2) specification language,
(3) sound and complete rules for proving the correctness of a program
with respect to its specification, and (4) tools for developing and
machine-checking formal proofs of correctness.  Evidence from the
literature indicates that such a combination could be established.  We
may admit that proving correctness is a difficult task--a task subject
to market forces and cost-benefit analysis.  But such proofs may have
high payback in critical systems.

Certainly a correctness proof, like any other proof, depends on
assumptions.  But proofs have the benefit of making their assumptions
explicit.

My claim is (1) that a proof provides better confidence of correctness
than either run-time assertion checking or testing some, but not all,
cases, and (2) that its cost may be justified for some, perhaps many,
applications.



-- 
Wayne D. Heym, Ph.D. Student,         NSFNet: <heym@cis.ohio-state.edu>
Computer and Information Science      Office: (614) 292-4898
The Ohio State University             Fax:    (614) 292-9021
Columbus, OHIO 43210-1277