comp.lang.ada
 help / color / mirror / Atom feed
From: Victor Porton <porton@narod.ru>
Subject: Preconditions which anyway would be caught?
Date: Sat, 09 Aug 2014 18:35:21 +0300
Date: 2014-08-09T18:35:21+03:00	[thread overview]
Message-ID: <ls5f3l$4t8$1@speranza.aioe.org> (raw)

function Inverse (X: Float) is
begin
   return 1/X;
end
   with Pre => (X /= 0);

Is this precondition superfluous? (it anyway could be caught by erroneous 
1/X operation)

-- 
Victor Porton - http://portonvictor.org


             reply	other threads:[~2014-08-09 15:35 UTC|newest]

Thread overview: 11+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2014-08-09 15:35 Victor Porton [this message]
2014-08-09 15:40 ` Preconditions which anyway would be caught? mockturtle
2014-08-09 16:08 ` Jeffrey Carter
2014-08-09 19:21 ` Peter Chapin
2014-08-09 19:24   ` Peter Chapin
2014-08-09 21:04     ` Niklas Holsti
2014-08-09 22:57       ` Peter Chapin
2014-08-10 20:58         ` Niklas Holsti
2014-08-10  7:24       ` Dmitry A. Kazakov
2014-08-11  0:00         ` Shark8
2014-08-11  7:31           ` Dmitry A. Kazakov
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox