80 lines
4.1 KiB
HTML
80 lines
4.1 KiB
HTML
<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. This should be obvious to anyone in the software industry.
|
|
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.
|
|
This is not enough. We need to be more complete, and we need to be more
|
|
precise. </p>
|
|
<p>Components based on object-oriented abstraction lend themselves perfectly to
|
|
a successful marriage with elements coming from the research on formal
|
|
specifikation. 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.
|
|
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. </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. If the corresponding
|
|
postcondition is false directly after a valid call, the error is on the supplier
|
|
side. 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.
|
|
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/">
|
|
"Building bug-free O-O Software"</a> for an overview, and
|
|
chapter eleven of his standard reference book on object-oriented concepts, "Object-Oriented
|
|
Software Construction", 2nd ed., Prentice Hall 1997, for a thorough explanation. For an
|
|
introductory book, see "Design by Contract by Example" 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 "Seamless Object-Oriented Software Architecture" 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> |