Re: Question: How usable is Linux Visual-Eiffel? One more question.

On Sat, 2006-01-07 at 10:56 +0100, H. v. L. wrote:
> I'd say that carefully chosen assertions are an equivalent to design by
> contract, a disciplined programmer will use those as he would use design
> by contract - or he won't use either of them.

There is a specialty of DbC that sets it apart from "just" assertions
(terminating the program), in two ways. First, DbC works starting
at the level of ADT modules, and ends at the level between
single statements. (This implies that you can specify module contracts
when there is no executable code yet.) In a sense, this structure
parallels stepwise refinement for assertions.

Second, DbC it is integrated with the language's exception
handling facilities.

Consider (in my pidgin Component Pascal)

MODULE Stacks;

TYPE
Stack* = POINTER TO ABSTRACT RECORD END;

PROCEDURE (s: VAR Stack) Pop*, ABSTRACT;




and in Eiffel

deferred class STACK feature

pop is
require
not_empty: not is_empty
deferred
end

How can I specify an assertion on abstract Pop* in CP?
Are there module assertions specifying an invariant?
Assertions are a Good Thing, but not quite the same as DbC :-)


-- Georg


.

Relevant Pages

  • Re: Design by contract and unit tests
    ... This is incorrect. ... prove the correctness of part of the contract (such as, for example, ... independent on whether assertions are evaluated at run-time or not. ... One of the most powerful ideas behind DbC is exactly to ...
    (comp.object)
  • Re: Applications of DBC
    ... defining DbC rigorously at any higher level of abstraction than ... that point validation will be solving the problem correctly. ... I suspect both the number of assertions and their complexity would ... level of collaboration rather than individual state machines. ...
    (comp.object)
  • DbC & TDD: Fizzing Fusion or Flat Fizzle? [2/2]
    ... an invariant is a general clause which ... information: the contract. ... The short form retains headers and assertions of exported features, ... exception handling -- handling abnormal cases. ...
    (comp.object)
  • Re: Question on LSP [LONG]
    ... No DbC holding while Liskov/Wing subtyping does not. ... The BASE contract explicitly stated ... Liskov also introduced a "constraint" clause ... A Liskov Constraint is effectively an added assertion to the post ...
    (comp.object)
  • Re: How to write testbench file?
    ... Assertions don't describe functionality; they scrutinize ... behaviour with the aim of finding violations of contract. ... simplification or optimization of the logic. ... match the original code's behaviour in simulation. ...
    (comp.lang.vhdl)