rule for checking contracts 
Author Message
 rule for checking contracts

Hello All,

 I have a question about rule for checking contracts. It seems to me that
current rules are not correspond with Liskov Substitution Principle. If we
have an weaken precondition - there is not difference how we use class - in
all cases weaken precondition is checked. But I think that in case we use
instance of child class through the reference to base class - weaken
precondition should not be checked.

Let`s see the example:

class PARENT
     foo ( param : INTEGER ) is
          require
               param > 0 and param < 10
          do end
end

class CHILD
     inherit PARENT redefine foo end
     foo ( param : INTEGER ) is
          require else
               param > 0 and param < 20
          do end
end

p : PARENT
c : CHILD

create p
create c

p.foo ( 9 )
-- p.foo ( 10 )  -- contract violation here, this is ok
c.foo ( 9 )
c.foo ( 10 ) -- this is ok

p := c
p.foo ( 10 ) -- there is not contract violation here - I think this is not
ok

I think that p.foo ( 10 ) we can use only if we already know that this is
reference to class CHILD, but this violates LSP. So I think that in this
case only contracts from class PARENT should be checked and should be
contract violation for p.foo ( 10 ). What Do You think ?

Best Regards, Alexey Lapshin.



Sat, 10 Apr 2004 00:45:04 GMT  
 rule for checking contracts
Hi Alexey,

1) You can't weaken a precondition.
2) I wrote about checking the actual class precondition instead of that of
the declared one some months ago, and some people said that it doesn't
matter, because the precondition is inherited anyway. I believe that is
completely wrong, but I understand the thinking. At least it makes the
compiler implementer's job simpler. But the practice of writing compilers in
that way makes them hide bugs in programs, which can be made apparent by
adding a subclass that violates no assertion, yet breaks the program.

Regards,

Peter van Rooijen


Quote:
> Hello All,

>  I have a question about rule for checking contracts. It seems to me that
> current rules are not correspond with Liskov Substitution Principle. If we
> have an weaken precondition - there is not difference how we use class -
in
> all cases weaken precondition is checked. But I think that in case we use
> instance of child class through the reference to base class - weaken
> precondition should not be checked.

> Let`s see the example:

> class PARENT
>      foo ( param : INTEGER ) is
>           require
>                param > 0 and param < 10
>           do end
> end

> class CHILD
>      inherit PARENT redefine foo end
>      foo ( param : INTEGER ) is
>           require else
>                param > 0 and param < 20
>           do end
> end

> p : PARENT
> c : CHILD

> create p
> create c

> p.foo ( 9 )
> -- p.foo ( 10 )  -- contract violation here, this is ok
> c.foo ( 9 )
> c.foo ( 10 ) -- this is ok

> p := c
> p.foo ( 10 ) -- there is not contract violation here - I think this is not
> ok

> I think that p.foo ( 10 ) we can use only if we already know that this is
> reference to class CHILD, but this violates LSP. So I think that in this
> case only contracts from class PARENT should be checked and should be
> contract violation for p.foo ( 10 ). What Do You think ?

> Best Regards, Alexey Lapshin.



Sat, 10 Apr 2004 06:29:46 GMT  
 rule for checking contracts

Quote:

>p : PARENT
>c : CHILD

>create p
>create c

>p.foo ( 9 )
>-- p.foo ( 10 )  -- contract violation here, this is ok
>c.foo ( 9 )
>c.foo ( 10 ) -- this is ok

>p := c
>p.foo ( 10 ) -- there is not contract violation here - I think this is not

I'm not sure I understand what your objection is, but there is indeed
a contract violation in that last line.  p is a PARENT, so unless you
have a really smart compiler, you must obey PARENT's contract.

The LSP says that if a program works with PARENT, it must also work
with CHILD.  The program you have provided wouldn't work with PARENT
in the first place, so LSP doesn't apply.

--
--
Patrick Doyle



Sat, 10 Apr 2004 08:37:16 GMT  
 rule for checking contracts

Quote:
> 1) You can't weaken a precondition.

According to Meyer's Object Oriented Software Construction (OOSC2),
you can weaken a precondition. See chapter 16 "Inheritance and
Assertions", particularly the Assertion Redeclaration rule on page
573: "A routine redeclaration may only replace the original
precondition by one equal or weaker, and the original postcondition by
one equal or stronger."

This rule seems completely intuitive to me. In fact, I recall that as
I was reading the book I had expected that it would probably work this
way, before I reached chapter 16.

I really don't understand this talk about making life easy for
"compiler implementers". Meyer's Assertion Redeclaration rule is meant
to make life easy for client-side programmers.



Sat, 10 Apr 2004 11:26:15 GMT  
 rule for checking contracts

Quote:
> > 1) You can't weaken a precondition.

Hi Peter,

Thanks for the correction. Seems I wasn't thinking when I wrote that. What's
your opinion on the other point?

Regards,

Peter van Rooijen

Quote:
> According to Meyer's Object Oriented Software Construction (OOSC2),
> you can weaken a precondition. See chapter 16 "Inheritance and
> Assertions", particularly the Assertion Redeclaration rule on page
> 573: "A routine redeclaration may only replace the original
> precondition by one equal or weaker, and the original postcondition by
> one equal or stronger."

> This rule seems completely intuitive to me. In fact, I recall that as
> I was reading the book I had expected that it would probably work this
> way, before I reached chapter 16.

> I really don't understand this talk about making life easy for
> "compiler implementers". Meyer's Assertion Redeclaration rule is meant
> to make life easy for client-side programmers.



Sat, 10 Apr 2004 14:32:29 GMT  
 rule for checking contracts
Patrick Doyle:

Quote:
> p is a PARENT, so unless you have a really smart compiler, you
> must obey PARENT's contract.

? I don't think any compiler checks contracts based on the static
type. The contract that is checked is the one in the dynamic type
(so weakened). The compiler need not be particularly smart to
implement that: the contract is part of the body of the routine
in the implementation, so is checked after dynamic dispatching.

Quote:
> The LSP says that if a program works with PARENT, it must also work
> with CHILD.  The program you have provided wouldn't work with PARENT
> in the first place, so LSP doesn't apply.

Agreed.


Sat, 10 Apr 2004 18:52:26 GMT  
 rule for checking contracts


Quote:


> >p : PARENT
> >c : CHILD

> >create p
> >create c

> >p.foo ( 9 )
> >-- p.foo ( 10 )  -- contract violation here, this is ok
> >c.foo ( 9 )
> >c.foo ( 10 ) -- this is ok

> >p := c
> >p.foo ( 10 ) -- there is not contract violation here - I think this is
not ok

> I'm not sure I understand what your objection is, but there is indeed
> a contract violation in that last line.  p is a PARENT, so unless you
> have a really smart compiler, you must obey PARENT's contract.

Hello Patrick,

But there was not contract violation in the last line. I have used ISE
Eiffel 5.0 demo. (I am not shure, but it seems to me that the same problem I
had met when used VisualEiffel 3.3 lite, unfortunately I can not check it
now). So, my objection is that I think contract violation *must be* in the
last line.

Quote:
> The LSP says that if a program works with PARENT, it must also work
> with CHILD.  The program you have provided wouldn't work with PARENT
> in the first place, so LSP doesn't apply.

But this program works with the reference to PARENT in the second place.
When this is possible:

p := c
p.foo ( 10 )

we are able to work with the parent like with a concrete child. If we will
use another child without redefined precondition we will have contract
violation. So this code just does not work for all possible children and
therefore breaks LSP.

I have read definition of LSP on www.objectmentor.com (search for lsp.pdf,
this document contains original text of LSP and paraphrase of this) :

"Functions that use pointers or references to base classes must be able to
use objects of derived classes without knowing it."

so, until there is not contract violation in the last line it is possible to
use p.foo ( 10 ) - only in case we already know that this is
reference to the derived class CHILD. In other cases this is impossible. So
I think without contract violation we able to write code that breaks LSP.

Best Regards, Alexey Lapshin.



Sat, 10 Apr 2004 19:12:58 GMT  
 rule for checking contracts

Quote:

>Patrick Doyle:

>> p is a PARENT, so unless you have a really smart compiler, you
>> must obey PARENT's contract.

>? I don't think any compiler checks contracts based on the static
>type. The contract that is checked is the one in the dynamic type
>(so weakened). The compiler need not be particularly smart to
>implement that: the contract is part of the body of the routine
>in the implementation, so is checked after dynamic dispatching.

Of course, you're right.  I tend to think that's a mistake, exactly
because of the LSP, so I always think of it as being checked before
the dispatch; but indeed, it is easy for a compiler to do the check
based on the class of the object, rather than the type of the
variable.

I think it's a bad idea though.  It would let you write code like this:

  class PARENT
  feature do_something( arg: INTEGER ) is
    require
      arg >= 0
    deferred
    end
  end

  class CHILD inherit PARENT
  feature do_something( arg: INTEGER ) is
    require else
      True
    deferred
    end
  end

  class CLIENT
  feature foo( p: PARENT ) is
    do
      p.do_something( -1 );
    end
  end

This seemingly obvious contract violation will not be caught if the
runtime system checks contracts based on runtime type, so long as
only instances of CHILD are passed to CLIENT.foo.  However, it seems
clear to me that this code is incorrect, so we'd like to use a policy
which would report an error.

Also, checking contracts based on the type of the variable is, I think,
a first step toward compile-time assertion checking.  I think this would
be impractical, if not impossible, if we had to use the class of the
object; and there seems to be no benefit.

--
--
Patrick Doyle



Sat, 10 Apr 2004 23:00:33 GMT  
 rule for checking contracts

Quote:





>> >p : PARENT
>> >c : CHILD

>> >create p
>> >create c

>> >p := c
>> >p.foo ( 10 ) -- there is not contract violation here - I think this is
>> >             -- not ok

>> I'm not sure I understand what your objection is, but there is indeed
>> a contract violation in that last line.  p is a PARENT, so unless you
>> have a really smart compiler, you must obey PARENT's contract.

>But there was not contract violation in the last line. I have used ISE
>Eiffel 5.0 demo. (I am not shure, but it seems to me that the same problem I
>had met when used VisualEiffel 3.3 lite, unfortunately I can not check it
>now). So, my objection is that I think contract violation *must be* in the
>last line.

Ah, I understand what you mean now.  As Franck pointed out in another
post, Eiffel compilers currently don't seem to check for this kind
of violation, and I think that's a flaw.

Quote:
>> The LSP says that if a program works with PARENT, it must also work
>> with CHILD.  The program you have provided wouldn't work with PARENT
>> in the first place, so LSP doesn't apply.

>But this program works with the reference to PARENT in the second place.
>When this is possible:

>p := c
>p.foo ( 10 )

What I meant is, if you call foo(10) on a PARENT, the program fails.
Thus, the LSP doesn't apply, so it makes no prediction as to what
happens if you call foo(10) on a CHILD.

Quote:
>I have read definition of LSP on www.objectmentor.com (search for lsp.pdf,
>this document contains original text of LSP and paraphrase of this) :

>"Functions that use pointers or references to base classes must be able to
>use objects of derived classes without knowing it."

Hmm, that's a paraphrasing I'm not quite comfortable with.  Besides the
fact that it's strongly oriented toward C++, the anthropomorphism of
functions (by stating what they should "know") detracts from the precision
of the original principle:

  "If for each object o1 of type S there is an object o2 of type T
  such that for all programs P defined in terms of T, the behavior
  of P is unchanged when o1 is substituted for o2 then S is a
  subtype of T."

If you read this carefully, you find that it is not what most people
say it is.  For one thing, it has nothing whatsoever to say about
abstract types, since it presupposes the existence of instances of
type T.

I think the spirit of the LSP is more important than its details.
A more useful definition of "subtype" might be along the lines of:

  "If for each correct program P defined in terms of a variable V of
  type T, the program remains correct when an object of type S is
  attached to V, then S is a subtype of T."

(Correctness here would imply that all contracts are satisfied.  The
concept of a "program" is left intentionally vague.)

This definition presupposes that a program can be shown to be correct
only in terms of its variables, not the dynamic types of objects.
To enforce this, it is necessary to check assertions based on the
static type of a variable, rather than the dynamic type of the object
to which it is attached.

Quote:
>so, until there is not contract violation in the last line it is possible to
>use p.foo ( 10 ) - only in case we already know that this is
>reference to the derived class CHILD. In other cases this is impossible. So
>I think without contract violation we able to write code that breaks LSP.

I think we reach the same conclusion, if perhaps we disagree on the details
of the LSP.  The "p.foo(10)" call should be illegal.

--
--
Patrick Doyle



Sat, 10 Apr 2004 23:34:46 GMT  
 rule for checking contracts

Quote:


> >Patrick Doyle:

> >> p is a PARENT, so unless you have a really smart compiler, you
> >> must obey PARENT's contract.

> >? I don't think any compiler checks contracts based on the static
> >type. The contract that is checked is the one in the dynamic type
> >(so weakened). The compiler need not be particularly smart to
> >implement that: the contract is part of the body of the routine
> >in the implementation, so is checked after dynamic dispatching.

> Of course, you're right.  I tend to think that's a mistake, exactly
> because of the LSP, so I always think of it as being checked before
> the dispatch; but indeed, it is easy for a compiler to do the check
> based on the class of the object, rather than the type of the
> variable.

> I think it's a bad idea though.  It would let you write code like this:

>   class PARENT
>   feature do_something( arg: INTEGER ) is
>     require
>       arg >= 0
>     deferred
>     end
>   end

>   class CHILD inherit PARENT
>   feature do_something( arg: INTEGER ) is
>     require else
>       True
>     deferred
>     end
>   end

>   class CLIENT
>   feature foo( p: PARENT ) is
>     do
>       p.do_something( -1 );
>     end
>   end

> This seemingly obvious contract violation will not be caught if the
> runtime system checks contracts based on runtime type, so long as
> only instances of CHILD are passed to CLIENT.foo.  However, it seems
> clear to me that this code is incorrect, so we'd like to use a policy
> which would report an error.

This is exactly the same problem that I described.

So, my suggestion is like Patrick proposed - check precondition for only
type of reference(not type of concrete inctance) which is known at compile
time.

Best Regards, Alexey Lapshin.



Sun, 11 Apr 2004 00:14:05 GMT  
 rule for checking contracts


Quote:
> Ah, I understand what you mean now.  As Franck pointed out in another
> post, Eiffel compilers currently don't seem to check for this kind
> of violation, and I think that's a flaw.

Agreed.

Quote:
> >I have read definition of LSP on www.objectmentor.com (search for
lsp.pdf,
> >this document contains original text of LSP and paraphrase of this) :

> >"Functions that use pointers or references to base classes must be able
to
> >use objects of derived classes without knowing it."

> Hmm, that's a paraphrasing I'm not quite comfortable with.  Besides the
> fact that it's strongly oriented toward C++, the anthropomorphism of
> functions (by stating what they should "know") detracts from the precision
> of the original principle:

Thank You, I will read Your interpretation of LSP more deeper and possible
will ask You some questions later.

Quote:

> >so, until there is not contract violation in the last line it is possible
to
> >use p.foo ( 10 ) - only in case we already know that this is
> >reference to the derived class CHILD. In other cases this is impossible.
So
> >I think without contract violation we able to write code that breaks LSP.

> I think we reach the same conclusion, if perhaps we disagree on the
details
> of the LSP.  The "p.foo(10)" call should be illegal.

Yes, It seems we do :-)

Best Regards, Alexey Lapshin.



Sun, 11 Apr 2004 00:36:24 GMT  
 rule for checking contracts


Quote:


> >so, until there is not contract violation in the last line it is possible
to
> >use p.foo ( 10 ) - only in case we already know that this is
> >reference to the derived class CHILD. In other cases this is impossible.
So
> >I think without contract violation we able to write code that breaks LSP.

> I think we reach the same conclusion, if perhaps we disagree on the
details
> of the LSP.  The "p.foo(10)" call should be illegal.

By the way, Patrick, What do You think about post-conditions ? Must post
conditions be checked according to dynamic type or static type ?

Best Regards, Alexey Lapshin.



Sun, 11 Apr 2004 00:57:30 GMT  
 rule for checking contracts
I am not a DBC expert (and my English is poor), but I would like to add a
few comments.  Correct me where I am wrong.  :-)

What is the meaning of a contract?

It is a logic implication.

If (client garantees parent PRE) -> (supplier garantees parent POST)

Since you probably have done logic classe, you know that it DOES NOT mean

If (client fails to garantee parent PRE) -> (supplier will not respect
parent POST)

However, it DOES MEAN

If (supplier dos not respect parent POST) -> (client has failed to garantee
parent PRE)

As far as I know, using the actual type of the object at run-time does not
break any of these rules.  Therefore, it is not incorrect.  Contracts must
catch calls that are incorrect, not those who programmers intuitively feel
are incorrect.  They don't catch virual contract violations, they catch real
violations.

From that perspective, it is OK, I think, for the run-time checking to be
performed on the type of the instance and not the type of the variable.  Not
doing so would, in a sense, reduce the power of polymorphism.  Why would you
use polymorphic calls on the methods but not on the assertions?

What if assertions are defined in terms of function calls?  Are you going to
use the parent version of the function call or the redefined child version?

I think things are fine as they are.  Then again, I don't have one tenth of
your experience and knowledge of computer langagues, so sorry if I am deeply
wrong here.



Sun, 11 Apr 2004 01:53:28 GMT  
 rule for checking contracts

Quote:

>By the way, Patrick, What do You think about post-conditions ? Must post
>conditions be checked according to dynamic type or static type ?

What do I think?

The short answer: postconditions should be checked on the dynamic type.

The medium answer: both the static and dynamic assertions should be
checked in all cases, because a failure in either case indicates a bug.
For preconditions, the static precondition must be at least as strong
as the dynamic one, so there is no need to check the dynamic one.  For
postconditions, and dynamic version must be at least as strong as the
static one, so only the dynamic version need be checked.

The long answer: the way I see it, types and classes are complementary.
Classes allow code to export a collection of features, while types allow
code to import them.  By declaring a variable of a certain type, you
are declaring what you expect of the object attached to that variable.
Then, by declaring a class, you are declaring what an object provides.

In Eiffel, every class declaration also declares an associated type,
since the moment you declare "class FOO", you can define a variable of
type FOO.  Every class automatically conforms to its own type, by
construction, since they are defined by the same code.  The rules
of DbC can be viewed as a mandate that every class must conform
to the types associated with all its superclasses.  (I don't
think this is the standard terminology, but it should be.  :-)

Both types and classes have contracts.  The contract of a type
describes what is expected of a variable, while the contract of
a class describes what is provided by an object.  All contracts
must be obeyed for a program to be correct.  That includes the
contracts imposed statically by a type, as well as those provided
dynamically be a class.

Thus, both the static and dynamic contracts must be fulfilled
in all cases.  However, as a matter of simplicity and optimization,
there is no need to check dynamic preconditions or static
postconditions, thanks to the rules of DbC.

The beauty of DbC, as I see it, is that a program's correctness can
be made apparent from a program's text.  This requires that any given
correctness property can be proven by inspecting a small amount of code
(or else the correctness is no longer "apparent").  Static contracts
reduce the amount of code that needs to be inspected, without posing
any significant constraints on the program.
--
--
Patrick Doyle



Sun, 11 Apr 2004 02:54:09 GMT  
 rule for checking contracts

Quote:

>What is the meaning of a contract?

>It is a logic implication.

>If (client garantees parent PRE) -> (supplier garantees parent POST)

Ok, so what does this tell you if client doesn't guarantee parent PRE?
Answer: nothing.

Quote:
>From that perspective, it is OK, I think, for the run-time checking to be
>performed on the type of the instance and not the type of the variable.  Not
>doing so would, in a sense, reduce the power of polymorphism.  Why would you
>use polymorphic calls on the methods but not on the assertions?

I think the power of DbC is in its ability to take dynamic behaviour
and relate it to the properties of the (static) source text.  That
is how it makes complex programs understandable.

Quote:
>What if assertions are defined in terms of function calls?  Are you going to
>use the parent version of the function call or the redefined child version?

Are you talking about returning to procedural programming?  In that
case, there's no dynamic dispatch, so the static and dynamic contracts
are always identical, and none of this makes any difference.

--
--
Patrick Doyle



Sun, 11 Apr 2004 03:21:02 GMT  
 
 [ 25 post ]  Go to page: [1] [2]

 Relevant Pages 

1. System level security check rules?

2. ASIS based the Ada rule checking tool gch for GNAT is available

3. CFP: RULE'02 - PLI-Workshop on Rule-Based Programming

4. CFP: RULE 2001 (2nd Int'l Workshop on Rule-based Programming)

5. CFP: RULE'02 - PLI-Workshop on Rule-Based Programming

6. CFP: RULE 2001 (2nd Int'l Workshop on Rule-based Programming)

7. RFI - Rule sets - pre-built - domain-specific foundation rules - availability or contacts

8. Contract, Contract-to-hire or permanent

9. JOBS - STVA - CONTRACT & CONTRACT TO PERMANENT

10. Contract Clarion Programmer and Contract Cobol Programmer/Analyst

11. "[Jobs] Contract, Contract-to-Hire,

12. "[Jobs] Contract, Contract-to-Hire,

 

 
Powered by phpBB® Forum Software