From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=0.7 required=5.0 tests=BAYES_00,INVALID_MSGID,
	PDS_OTHER_BAD_TLD autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: fac41,9a0ff0bffdf63657
X-Google-Attributes: gidfac41,public
X-Google-Thread: 1108a1,9a0ff0bffdf63657
X-Google-Attributes: gid1108a1,public
X-Google-Thread: 103376,4b06f8f15f01a568
X-Google-Attributes: gid103376,public
X-Google-Thread: f43e6,9a0ff0bffdf63657
X-Google-Attributes: gidf43e6,public
From: Matthew Heaney <matthew_heaney@acm.org>
Subject: Re: Software landmines (loops)
Date: 1998/09/17
Message-ID: <m3n27z6ccv.fsf@mheaney.ni.net>#1/1
X-Deja-AN: 391918419
Sender: matt@mheaney.ni.net
References: <slrn6sopmg.4fg.jdege@jdege.visi.com> <35f51e53.480
 <904556531.66622 <EyyLos.2nx@yc.estec.esa.nl>
 <6t4dmi$rhp@flatland.dimensional.com> <35F712BD.4F521172@earthlink.net>
NNTP-Posting-Date: Wed, 16 Sep 1998 20:12:05 PDT
Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.lang.ada
Date: 1998-09-17T00:00:00+00:00
List-Id: <comp.lang.ada>

Charles Hixson <charleshixsn@earthlink.net> writes:

> It has been claimed that Design By Contract (DBC) can be done entirely
> by comments and documentation.  I, personally, don't believe it.  It is
> my expectation that the routines with explicit pre-conditions and
> post-conditions would work as desired in the Eiffel environment, where
> the developer could have pre-conditions enabled while developing it, and
> only remove them (IN LAYERS!) when the final code was produced.  I don't
> think that this would work at all as well without support from the IDE.
> 
> Now it is true, that the failures of DBC in an environment that doesn't
> support it can be traced to the contract not being lived up to, but
> ENFORCEABILITY IS A PART OF THE CONTRACT.  In an environment that
> doesn't enforce the contract, violations will not be detected, and I
> don't know about you, but my programs always need to have the bugs
> cleaned out of them before they are ready for delivery.

Use assertions to check preconditions.  When you're satisfied everyone
is obeying them, then recompile the body with assertions turned off:

function Get_Top (Stack : Stack_Type) return Stack_Item is
begin
   pragma Assert (Stack.Top /= 0);
...
end Get_Top;

You can even use a controlled type to check that a representation
invariant is being satisfied on procedure entry and exit.