question about strengthened post-conditions

[Mirabelle Nebut-2]

Hello,

There is something I do not understand with JML postcondition
inheritance. I've explained to students what is behavioral inheritance
and how it works using JML according to :
ftp://ftp.cs.iastate.edu/pub/techreports/TR06-22/TR.pdf
After the practical work, one of the student complained that its
contracts were not violated by a wrong code. Looking for the mistake, I
found that even the post-condition "ensures false" was accepted by
jmlrac ! I guess there is either something I do not understand at all,
or a bug in jmlc.

I give here a very simple example which shows what does work
(inheritance of a whole specification and of pre-conditions) and what
does not (strengthened post-condition). I join an interface Mother.java
and a class Daughter.java which implements Mother.

There are an integer model attribute i and 3 methods :
- increment
- decrement
- set(int)

For set(int) : the whole specification is inherited by Daughter, and I
checked (see the main in Daughter) that both the Mother's pre and post
are violated by adequate calls (the code is wrong).

For decrement() : the daugther inherits the precondition of Mother with
\same, and adds some postconditions. I checked it indeed has the
postcondition of its mother (wrong code which violates the mother's
postcond).

For increment() : same pattern, but the code only violates the
daugther's postcond... and nothing happens.

nebut@soy:~/ENSEIGNEMENT/SVL/progContrats/essaiAlso$ jmlc --version
usage: org.jmlspecs.jmlrac.Main [option]* [--help] <jml-files>
Version: Common JML release 5.5 (January 9, 2008)
nebut@soy:~/ENSEIGNEMENT/SVL/progContrats/essaiAlso$ jmlrac Daughter
nebut@soy:~/ENSEIGNEMENT/SVL/progContrats/essaiAlso$

If someone can help me...

Another question : I think it is the last year I can ask administators
to install java4 only for the JML course... is there a chance that
JML"java5" will be available in january 2009 ? I tried ModernJass to
avoid using java4, but I encountered problems with simple programs and
drop it.

Cheers,

Mirabelle.
--
Mirabelle Nebut - mailto:Mirabelle.Nebut@...
Maître de conférences - Université de Lille 1
tel: +(33|0) 3 28 77 85 70
http://www.lifl.fr/~nebut

public class Daughter implements Mother {

    //@ private represents i <- _i;
    private int _i; //@ in i;

    public Daughter() {
        this._i = 0;
    }

    /*@ also
      @ requires \same;
      @ ensures i == \old(i) + 1;
      @ ensures false;
      @*/
    public void increment() {
        this._i = this._i + 2;
    }

    /*@ also
      @ requires \same;
      @ ensures i == \old(i) - 1;
      @ ensures false;
      @*/
    public void decrement() {
        this._i = this._i + 2;
    }


    public void set(int x) {
        this._i = x-1;
    }


    public void correctSet(int x) {
        this._i = x;
    }

    public static void main(String arg[]) {
        Daughter d = new Daughter();
        // d.set(-3); // violates mother's precond : OK
        // d.set(3); // violates mother's postcond : OK
        // d.correctSet(-3); d.increment(); // violates mother's precond : OK
        d.increment(); // should violate daugther's postcond : KO
        // d.decrement(); // violates mother's postcond : OK
    }
}
public interface Mother {

    //@ public instance model int i;

    /*@ requires i>= 0;
      @ assignable i;
      @ ensures i > \old(i);
      @*/
    public void increment();

    /*@ requires i>= 0;
      @ assignable i;
      @ ensures i < \old(i);
      @*/
    public void decrement();


    //@ ensures i == x;
    public void set(int x);

   


}
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest

[Wladimir de Lara Araujo Filho]

        Hi, Mirabelle,

        The problem is with the specification and with jmlc. From a
specification point of view, Daughter.increment() has the following
effective specification (ignoring the assignable clause):

requires i >= 0 || i >= 0;
ensures (\old(i >= 0) ==> i > \old(i)) && (\old(i >= 0) ==> (i ==
\old(i) + 1) && false);

The first term comes from Mother and the second from Daughter. By
looking at the spec, one can see that Daughter is NOT a behavioural
subtype of Mother, although the implementation is.

Jmlc cannot handle this. It assumes that specifications are consistent.
Given that, from jmlc's point of view, the specification really is:

requires i >= 0 || false; /* false comes from \same */
ensures (\old(i >= 0) ==> i > \old(i)) && (\old(i >= 0) ==> (i ==
\old(i) + 1) && false);

This effectively means that it is trusting the specifier designed
consistent postconditions, i.e. that i > \old(i) ==> i == \old(i) + 1)
&& false, which we know is not the case. This is because jmlc cannot
know its supertype's specifications due to the separate compilation
requirement. Otherwise, it could've copied down the desugared
preconditions (i.e. their disjunction) in place of \same. That would
produce the effect you expected.

I hope I made sense.

        Cheers,

Wladimir de Lara Araujo Filho
260 Besserer St. suite 602
Ottawa-ON Canada
K1N 1J3
Phone [phone]

There are three schools of magic.
One: State a tautology, then ring the changes on its
corollaries;  that's philosophy.
Two: Record many facts. Try to find a pattern.
Then make a wrong guess at the next fact; that's science.
Three: Be aware that you live in a malevolent Universe controlled
by Murphy's Law, sometimes offset by
Brewster's Factor; that's engineering.
-- Robert A. Heinlein


> -----Original Message-----
> From: jmlspecs-interest-bounces@...
[mailto:jmlspecs-
> interest-bounces@...] On Behalf Of Mirabelle Nebut
> Sent: February 23, 2008 12:19 PM
> To: jmlspecs-interest@...
> Subject: [Jmlspecs-interest] question about strengthened
post-conditions
>
> Hello,
>
> There is something I do not understand with JML postcondition
> inheritance. I've explained to students what is behavioral inheritance
> and how it works using JML according to :
> ftp://ftp.cs.iastate.edu/pub/techreports/TR06-22/TR.pdf
> After the practical work, one of the student complained that its
> contracts were not violated by a wrong code. Looking for the mistake,
I
> found that even the post-condition "ensures false" was accepted by
> jmlrac ! I guess there is either something I do not understand at all,
> or a bug in jmlc.
>
> I give here a very simple example which shows what does work
> (inheritance of a whole specification and of pre-conditions) and what
> does not (strengthened post-condition). I join an interface
Mother.java

> and a class Daughter.java which implements Mother.
>
> There are an integer model attribute i and 3 methods :
> - increment
> - decrement
> - set(int)
>
> For set(int) : the whole specification is inherited by Daughter, and I
> checked (see the main in Daughter) that both the Mother's pre and post
> are violated by adequate calls (the code is wrong).
>
> For decrement() : the daugther inherits the precondition of Mother

with

> \same, and adds some postconditions. I checked it indeed has the
> postcondition of its mother (wrong code which violates the mother's
> postcond).
>
> For increment() : same pattern, but the code only violates the
> daugther's postcond... and nothing happens.
>
> nebut@soy:~/ENSEIGNEMENT/SVL/progContrats/essaiAlso$ jmlc --version
> usage: org.jmlspecs.jmlrac.Main [option]* [--help] <jml-files>
> Version: Common JML release 5.5 (January 9, 2008)
> nebut@soy:~/ENSEIGNEMENT/SVL/progContrats/essaiAlso$ jmlrac Daughter
> nebut@soy:~/ENSEIGNEMENT/SVL/progContrats/essaiAlso$
>
> If someone can help me...
>
> Another question : I think it is the last year I can ask administators
> to install java4 only for the JML course... is there a chance that
> JML"java5" will be available in january 2009 ? I tried ModernJass to
> avoid using java4, but I encountered problems with simple programs and
> drop it.
>
> Cheers,
>
> Mirabelle.
> --
> Mirabelle Nebut - mailto:Mirabelle.Nebut@...
> Maître de conférences - Université de Lille 1
> tel: +(33|0) 3 28 77 85 70
> http://www.lifl.fr/~nebut

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest

[Mirabelle Nebut-2]

Hello,

Thanks Wladimir for your quick answer. Unfortunately I'm afraid I still
 do not understand :(

Let's drop the "assignable false" which is striking but confusing, and
take an incrementBis() specification :

For the Mother interface :

   /*@ requires i>= 0;
      @ assignable i;
      @ ensures i > \old(i);
      @*/
    public void incrementBis();

For the Daughter class :

    /*@ also
      @ requires \same;
      @ ensures i == \old(i) + 1;
      @*/
    public void incrementBis() {
        this._i = this._i + 2;
    }

Wladimir de Lara Araujo Filho wrote:
> Hi, Mirabelle,
>

> requires i >= 0 || i >= 0;
> ensures (\old(i >= 0) ==> i > \old(i)) && (\old(i >= 0) ==> (i ==
> \old(i) + 1) && false);

Now we get :

requires i >= 0 || i >= 0; // or i >= 0 || false
ensures (\old(i >= 0) ==> i > \old(i))
        && (\old(i >= 0) ==> (i == \old(i) + 1));

which is exactly what I need.

> The first term comes from Mother and the second from Daughter. By
> looking at the spec, one can see that Daughter is NOT a behavioural
> subtype of Mother, although the implementation is.
> Jmlc cannot handle this. It assumes that specifications are consistent.
> Given that, from jmlc's point of view, the specification really is:
>
> requires i >= 0 || false; /* false comes from \same */
> ensures (\old(i >= 0) ==> i > \old(i)) && (\old(i >= 0) ==> (i ==
> \old(i) + 1) && false);
>
> This effectively means that it is trusting the specifier designed
> consistent postconditions, i.e. that i > \old(i) ==> i == \old(i) + 1)
> && false, which we know is not the case.

I do not understand why Daughter is not a subtype of Mother. I would
have written the opposite "obligation proof" of yours (I thought the
postcond of the subtype is assumed to imply the postcond of the
supertype, since the former strengthens the later) :
(i == \old(i) + 1) ==> (i > \old(i))
I do not see what is inconsistent here at the level of the specification ?
The code is not consistent with the specification, since it conforms to
i >=0 ==> i > \old(i) (Mother), but not to i >= 0 ==> i == \old(i) + 1
(Daughter).

>This is because jmlc cannot
> know its supertype's specifications due to the separate compilation
> requirement. Otherwise, it could've copied down the desugared
> preconditions (i.e. their disjunction) in place of \same. That would
> produce the effect you expected.

I'm not sure I understand : here I have a problem with the subtype
specification whose postcondition should be violated by any call to
incrementBis() in a state where i >= 0 (But jmlrac does not complain).

Cheers,

Mirabelle.
--
Mirabelle Nebut - mailto:Mirabelle.Nebut@...
Maître de conférences - Université de Lille 1
tel: +(33|0) 3 28 77 85 70
http://www.lifl.fr/~nebut

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest

[Wladimir de Lara Araujo Filho]

        Hi, Mirabelle,

        Sorry for the late response. We might need Gary's input because
I always get confused with behaviour subtyping rules :)

                Cheers,

Wladimir de Lara Araujo Filho
260 Besserer St. suite 602
Ottawa-ON Canada
K1N 1J3
Phone [phone]

There are three schools of magic.
One: State a tautology, then ring the changes on its
corollaries;  that's philosophy.
Two: Record many facts. Try to find a pattern.
Then make a wrong guess at the next fact; that's science.
Three: Be aware that you live in a malevolent Universe controlled
by Murphy's Law, sometimes offset by
Brewster's Factor; that's engineering.
-- Robert A. Heinlein


> -----Original Message-----
> From: jmlspecs-interest-bounces@...
[mailto:jmlspecs-

> interest-bounces@...] On Behalf Of Mirabelle Nebut
> Sent: February 24, 2008 3:30 PM
> To: Wladimir de Lara Araujo Filho
> Cc: jmlspecs-interest@...
> Subject: Re: [Jmlspecs-interest] question about strengthened post-
> conditions
>
> Hello,
>
> Thanks Wladimir for your quick answer. Unfortunately I'm afraid I

still

>  do not understand :(
>
> Let's drop the "assignable false" which is striking but confusing, and
> take an incrementBis() specification :
>
> For the Mother interface :
>
>    /*@ requires i>= 0;
>       @ assignable i;
>       @ ensures i > \old(i);
>       @*/
>     public void incrementBis();
>
> For the Daughter class :
>
>     /*@ also
>       @ requires \same;
>       @ ensures i == \old(i) + 1;
>       @*/
>     public void incrementBis() {
> this._i = this._i + 2;
>     }
>
> Wladimir de Lara Araujo Filho wrote:
> > Hi, Mirabelle,
> >
>
> > requires i >= 0 || i >= 0;
> > ensures (\old(i >= 0) ==> i > \old(i)) && (\old(i >= 0) ==> (i ==
> > \old(i) + 1) && false);
>
> Now we get :
>
> requires i >= 0 || i >= 0; // or i >= 0 || false
> ensures (\old(i >= 0) ==> i > \old(i))
>         && (\old(i >= 0) ==> (i == \old(i) + 1));
>
> which is exactly what I need.

[Wladimir Araujo]
This works.

The only problem now is with the RAC. If you replace \same with the same
requires clause of Mother, Daughter will behave as you expect.

>
> > The first term comes from Mother and the second from Daughter. By
> > looking at the spec, one can see that Daughter is NOT a behavioural
> > subtype of Mother, although the implementation is.
> > Jmlc cannot handle this. It assumes that specifications are
consistent.
> > Given that, from jmlc's point of view, the specification really is:
> >
> > requires i >= 0 || false; /* false comes from \same */
> > ensures (\old(i >= 0) ==> i > \old(i)) && (\old(i >= 0) ==> (i ==
> > \old(i) + 1) && false);
> >
> > This effectively means that it is trusting the specifier designed
> > consistent postconditions, i.e. that i > \old(i) ==> i == \old(i) +
1)
> > && false, which we know is not the case.
>
> I do not understand why Daughter is not a subtype of Mother. I would
> have written the opposite "obligation proof" of yours (I thought the
> postcond of the subtype is assumed to imply the postcond of the
> supertype, since the former strengthens the later) :
> (i == \old(i) + 1) ==> (i > \old(i))
> I do not see what is inconsistent here at the level of the
specification ?
> The code is not consistent with the specification, since it conforms
to
> i >=0 ==> i > \old(i) (Mother), but not to i >= 0 ==> i == \old(i) + 1
> (Daughter).
[Wladimir Araujo]
That you'd have to take a look at Gary's papers. The problem was with
the 'false' part. Daughter presented a different behaviour than Mother
for the same precondition. That, AFAIK, characterizes a breakage on
behavioural subtyping. But I'd defer to Gary for the final word on it.

>
> >This is because jmlc cannot
> > know its supertype's specifications due to the separate compilation
> > requirement. Otherwise, it could've copied down the desugared
> > preconditions (i.e. their disjunction) in place of \same. That would
> > produce the effect you expected.
>
> I'm not sure I understand : here I have a problem with the subtype
> specification whose postcondition should be violated by any call to
> incrementBis() in a state where i >= 0 (But jmlrac does not complain).
>

[Wladimir Araujo]
Let me show you how the RAC works with a generic example. For class A,
method m() we have the following spec:

requires P1;
ensures Q1;
also requires P2;
ensures Q2;
also requires \same;
ensures Q3;

This is desugared to:

requires P1 || P2 || (P1 || P2); // the last term is the effect of \same
ensures (\old(P1) ==> Q1) && (\old(P2) ==> Q2) && (\old(P1 || P2) ==>
Q3);

If the RAC translated \same as above, Q3 would be evaluated as part of
the execution of m(). However, the RAC is assuming that Q1 || Q2 ==> Q3,
so \same is translated to false and Q3 is never actually evaluated.
That's why you see the unexpected behaviour you reported.

BTW, that's the behaviour with JML 5.4_rc2. This might've been fixed in
later releases. Just to confirm this is the problem you are seeing,
could you please 'jmlc -P Daughter.java'? I can then see the generated
code and verify if this is indeed the problem. You can send this to me
in pvt.

> Cheers,
>
> Mirabelle.
> --
> Mirabelle Nebut - mailto:Mirabelle.Nebut@...
> Maître de conférences - Université de Lille 1
> tel: +(33|0) 3 28 77 85 70
> http://www.lifl.fr/~nebut
>
>

------------------------------------------------------------------------
-
> This SF.net email is sponsored by: Microsoft
> Defy all challenges. Microsoft(R) Visual Studio 2008.
> http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> _______________________________________________
> Jmlspecs-interest mailing list
> Jmlspecs-interest@...
> https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest


-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest

[Wladimir de Lara Araujo Filho]

>
> No, in JML all subtypes are behavioral subtypes of their supertypes by
> specification inheritance.  They may not be implentable, and Daughter
> is not implementable, since it has a postcondition that can't be
> satisfied.
[Wladimir Araujo]
That's what I meant. Thanks for clarifying this.

>
> > Jmlc cannot handle this. It assumes that specifications are
consistent.
>
> No, jmlc should be able to give assertion violations from inconsistent
> specifications.   It does not need to and does not assume that
> specifications are consistent.
[Wladimir Araujo]
Since this is a bug, I will file a bug report.
For now, then, \same does not work on jmlc. As a workaround, you can
just replace \same with the expected desugaring, which, for
preconditions, is the disjunction of all inherited preconditions.

I don't know what the semantics is for postconditions. Can someone
clarify this?

>
>          Gary T. Leavens
>          210 Harris Center (Bldg. 116)
>          School of EECS, University of Central Florida
>          4000 Central Florida Blvd., Orlando, FL 32816-2362 USA
>          http://www.eecs.ucf.edu/~leavens  phone: [phone]
>          leavens@...


-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest