Re: Programming with Contracts
Posted: Oct 17, 2004 10:01 PM
> Hi Roger,
> DbC is a software design methodology using the abstract
> notion of concepts, where is PwC refers to the usage of
> contracts in the software.
I'm puzzled by this. Are you saying the PwC is the use of assertions to check contracts?
>Designing software is a task
> separate from implementation.
Sadly, this is a misconception held by many. I agree that things such as (for example) creating a UML class diagram and Responsibility Driven Design are high-level design activities and are distinct from implementation (i.e. writing code). However, implementation is itself a design activity, albeit at much lower level of abstraction. Nonetheless, defining the control structure and data flow of a program (procedure,method) are design activities in and of themselves. Unfortunately, both the software industry and academia have forgotten this.
Now as to DbC vs PwC, if the answer to my question posed above is "yes", then I am really puzzled. In particular, what learned as DbC back in the late 80's and into the 90's includes the use of assertions to check contracts, invariants, assumptions, and the like.
> I could use the abstract
> notion of contracts to express my software design whether
> or not I actually implement some kind of contract
> verification in my code.
Agreed, but this is not new. This has always been the case with DbC, so what does PwC offer that is not already in DbC? Or, is PwC simply the result of refactoring DbC into distinct design and programming components?
>The same thing applies to Object
> Oriented Design. I can theoertically use OOD and UML to
> design a C program. I am not arguing these are good ideas,
> but that design is a separate practice from
There is no theory to it. It has been done before. As to being good ideas, why would they not be?
> Christopher said:
> "If a clause is ever violated, there is a defect in your
> software (or possibly your contract)."
> Roger said: "You parenthetical comment impkies that the
> specification is wrong. But were there were a contract
> violation (i.e. a clause if false, which could only occur
> during the execution of a method), then the method's
> implementation is incorrect in the first place. This
> assumes the contract is specified *before* the method is
> implemented. If this is not the case, the contract could
> be incorrect. However, this should only be a possibility
> when contracts are derived as part of reverse engineering
> (i.e. they were not specified in the first place or they
> were lost). The should not be the result of a
> dysfunctional development practice whereby the code is
> written first and then the contracts are specified. Sadly,
> I know this is not an uncommon practice."
> I agree that DbC specifies that contracts should be
> written before implementation. It is reasonable though to
> expect that a contract will occasionally have an error, in
> the same way that DbC is based on the assumption that code
> will have errors. I don't see how reverse engineering is
> neccessary for a contractual error. I commonly mistakenly
> write contractual clauses that are incompatible with each
I see, you are pointing out that contracts must be self-consistent. That is, their clauses cannot equate to false. You are right, this is certainly a possibility, perhaps a common reality. But, it still is the case that the specification is flawed, and in this type of situation, no program can be written that will satisfy such a specification. Note that this argument assumes that the specification is written before the implementation. Also, I am making the distinction between the contract as specification and use of assertions to verify that contracts hold in a particular implementation. These are distinct.
Also implicit in my argument is that the specification is written first and then the implementation is written to the specification. Yes, I know that this is not always done, that folks often write the code and the specification simultaneously, with the code in effect being the specification.
> Roger said: "You are correct that exceptions and system
> failures are error conditions, but they are contract
> violations if they can occur and the specification of a
> method does not include them include them in its
> postcondition (assuming the method does not handle the
> exception or system failure). Putting it differently, if
> the occurrence of an exception or system failure prevents
> a method from establishing its postcondition, then a
> contract violation occurs. Period."
> I agree with you here. I don't see where there is
> contention. Perhaps my description was not well worded?
No contention intended, just clarification. I too have experience and knowledge, and am on a quest for truth.