CSC/ECE 517 Fall 2007/wiki3 2 at: Difference between revisions

From Expertiza_Wiki
Jump to navigation Jump to search
Line 26: Line 26:
<br>
<br>


Such properties are part of the abstract data type specification, and even people who do not use any approach remotely as formal as ADTs understand them implicitly. But in common approaches to software construction software texts reveal no trace of them. Through routine preconditions and postconditions you can turn them into explicit elements of the software.
Such properties are part of the abstract data type specification, and even people who do not use any approach remotely as formal as ADTs understand them implicitly. But in common approaches to software   construction software texts reveal no trace of them. Through routine preconditions and postconditions you can turn them into explicit elements of the software.


<pre>
<pre>
indexing
 
description: "Stacks: Dispenser structures with a Last-In, First-Out %
%access policy"
class STACK1 [G] feature -- Access
class STACK1 [G] feature -- Access
count: INTEGER
    count: INTEGER
-- Number of stack elements
            -- Number of stack elements
item: G is
    item: G is
-- Top element
                -- Top element
require
            require
not empty
            not empty
do
            do
¼
              ....
end
            end
 
feature -- Status report
feature -- Status report
empty: BOOLEAN is
    empty: BOOLEAN is
-- Is stack empty?
                -- Is stack empty?
do ¼ end
            do  
full: BOOLEAN is
              ....
-- Is stack representation full?
            end
do
 
¼
    full: BOOLEAN is
end
                -- Is stack representation full?
            do
              ....   
            end
 
feature -- Element change
feature -- Element change
put (x: G) is
    put (x: G) is
-- Add x on top.
                -- Add x on top.  
require
            require
not full
                not full
do
            do
¼
                ....
ensure
            ensure
not empty
                not empty
item = x
                item = x
count = old count + 1
                count = old count + 1
end
            end
remove is
 
-- Remove top element.
    remove is
require
                  -- Remove top element.
not empty
            require
do
                not empty
¼
            do
ensure
                ....
not full
            ensure
count = old count – 1
                not full
end
                count = old count – 1
            end
end
end
</pre>
</pre>

Revision as of 18:58, 27 November 2007

Topic:
In class, we had some difficulty coming up with good examples of programming by contract. Find some concise ones that illustrate the principle well, and are accessible to a general audience of programmers.

Programming by contract

Programming by Contract is a way of specifying the behavior of a function, and the name arises from its formal similarity to a legal contract. The key concept is viewing the relationship between a class and its clients as a formal agreement, expressing each party’s rights and obligations. Defining a precondition and a postcondition for a routine is a way to define a contract that binds the routine and its callers. The precondition states the properties that must hold whenever the routine is called; the postcondition states the properties that the routine guarantees when it returns.
By associating clauses require pre and ensure post with a routine r, the class tells its clients:

If you promise to call r with pre satisfied then I, in return, promise to deliver a final state in which post is satisfied.


Consider the following example:

class STACK [G] feature
 ...Declaration of the features:
    count, empty, full, put, remove, item
end

Before considering implementation issues, however, it is important to note that the routines are characterized by strong semantic properties, independent of any specific representation.

For example:
• Routines remove and item are only applicable if the number of elements is not zero.
put increases the number of elements by one; remove decreases it by one.

Such properties are part of the abstract data type specification, and even people who do not use any approach remotely as formal as ADTs understand them implicitly. But in common approaches to software construction software texts reveal no trace of them. Through routine preconditions and postconditions you can turn them into explicit elements of the software.


class STACK1 [G] feature -- Access
     count: INTEGER
            -- Number of stack elements
     item: G is
                 -- Top element
            require
            not empty
            do
               .... 
            end

feature -- Status report
     empty: BOOLEAN is
                 -- Is stack empty?
            do 
               ....
            end

     full: BOOLEAN is
                 -- Is stack representation full?
            do
               ....     
            end

feature -- Element change
     put (x: G) is
                 -- Add x on top. 
            require
                not full
            do
                .... 
            ensure
                not empty
                item = x
                count = old count + 1
            end

     remove is
                  -- Remove top element.
            require
                not empty
            do
                .... 
            ensure
                not full
                count = old count – 1
            end
end

See Also

http://en.wikibooks.org/wiki/Computer_programming/Design_by_Contract
http://www.eventhelix.com/RealtimeMantra/Object_Oriented/design_by_contract.htm
http://www.cs.uno.edu/~c1581/Labs2006/lab7/lab7.htm
http://www.phpunit.de/pocket_guide/3.2/en/test-first-programming.html
http://www.python.org/dev/peps/pep-0316/
http://www.artima.com/cppsource/deepspace2.html
http://java.sun.com/j2se/1.4.2/docs/guide/lang/assert.html
http://www.csc.calpoly.edu/~dstearns/SeniorProjectsWWW/Rideg/dbc.html

References

[1] http://www.ibm.com/developerworks/rational/library/455.html#N10324
[2] http://archive.eiffel.com/doc/manuals/technology/contract/page.html
[3] http://www.wayforward.net/pycontract/
[4] http://www.patentstorm.us/patents/6442750-description.html
[5] http://www.open-std.org/JTC1/SC22/WG21/docs/papers/2004/n1613.pdf