Imported from archive

This commit is contained in:
Eiffel operator
2026-03-25 07:12:09 -08:00
commit b929708190
75 changed files with 7823 additions and 0 deletions

80
www/contracts_main.htm Normal file
View File

@@ -0,0 +1,80 @@
<html>
<head>
<meta http-equiv="Content-Language" content="sv">
<meta name="GENERATOR" content="Microsoft FrontPage 5.0">
<meta name="ProgId" content="FrontPage.Editor.Document">
<meta http-equiv="Content-Type" content="text/html; charset=windows-1252">
<meta name="author" content="Kim Walden">
<title>BON method: Design by Contract main</title>
<base target="_self">
<link rel="stylesheet" type="text/css" href="nn4.css">
<style type="text/css">
@import url("normal.css");
</style>
<script type="text/javascript">
<!--
if (navigator.userAgent.indexOf("MSIE")!=-1)
document.write('<link rel="stylesheet" type="text/css" href="ie.css">')
function check() {
if (top.frames.length == 0 || top.frames[0].name != "banner")
top.location.href = "index.htm?contracts";
}
//-->
</script>
</head>
<body onload="check()" bgcolor="#ffffff" alink="#33cc00" link="#0000ff" vlink="#0000ff">
<h1>Design by Contract</h1>
<p>Software components whose behavior is not completely specified cannot be
trusted.&nbsp; This should be obvious to anyone in the software industry.&nbsp;
And yet the majority of systems out there are made up of parts most of which are
only (at best) partially specified, usually by natural language comments.&nbsp;
This is not enough.&nbsp; We need to be more complete, and we need to be more
precise.&nbsp; </p>
<p>Components based on object-oriented abstraction lend themselves perfectly to
a successful marriage with elements coming from the research on formal
specifikation.&nbsp; Objects offer their services through operations that can be
furnished with pre- and postconditions expressed as simple boolean expressions
involving the supplied arguments, if any, and the current state of the object.&nbsp;
The precondition stipulates what must be fulfilled before a client is allowed to
invoke the operation, and the postcondition specifies what is guaranteed to be
fulfilled directly after the call, provided that the precondition was true at
the time of invocation.&nbsp; </p>
<p>If a precondition is false at the time of the call, this constitutes an error
on behalf of the client, and the call is invalid.&nbsp; If the corresponding
postcondition is false directly after a valid call, the error is on the supplier
side.&nbsp; Besides pre- and postconditions, which specify the behavior of
individual operations, a class invariant can be added which specifies general
conditions that must always be true before and after a call to any operation.&nbsp;
Invariants tell you something about the inherent properties of the whole
abstraction, as opposed to the behaviors of individual operations.</p>
<p>Using formal specification in this way gives us double advantages:</p>
<ul>
<li class=bullet><p class="bullet">contrary to human language, the assertions are precise, leaving no doubt
about what is really meant </p></li>
<li class=bullet><p class="bullet">the specifications can be used as basis for a disciplined exception
handling mechansim and for automatic assertion checking at run-time, yielding
a very powerful debugging aid </p></li>
</ul>
<p>Design by contract was invented by Bertrand Meyer, see his article
<a target="_blank" href="http://archive.eiffel.com/doc/manuals/technology/contract/">
&quot;Building bug-free O-O Software&quot;</a> for an overview, and
chapter eleven of his standard reference book on object-oriented concepts, &quot;Object-Oriented
Software Construction&quot;, 2nd ed., Prentice Hall 1997, for a thorough explanation.&nbsp; For an
introductory book, see &quot;Design by Contract by Example&quot; by James McKim and Richard
Mitchell, Addison Wesley 2001.</p>
<p>See also <a target="_blank" href="pages%20205-212%20from%20book_print_a4.pdf">pp. 205-212
</a>in &quot;Seamless Object-Oriented Software Architecture&quot; and a presentation
at the web site of Eiffel Software,
<a href="http://www.eiffel.com/developers/presentations/dbc/partone/player.html?slide=">
part 1</a> and
<a href="http://www.eiffel.com/developers/presentations/dbc/parttwo/player.html?slide=">
part 2</a>.</p>
</body>
</html>