Issue to understand the log

[GabrielHerry]

Hello,

My error is certainly obvious but behind that, I wonder how I can understand-interpret better the result of the JML-log & JML-Trace with OpenJML Eclipse plugin and z3_4_3.

Here my code and JML-log :

`package jmltest;

import java.util.ArrayList;

public class ListTest {

private final /*@ spec_public  @*/ ArrayList<String> mylist;

public /*@ pure @*/ ArrayList<String> getMylist() {

	return mylist;}

public ListTest() {

	mylist = new ArrayList<String>();}

//@ ensures  \old(getMylist()).size() + 1 == getMylist().size()  ; 

public void addStringInList(String a){

	this.mylist.add(a);

}

}
`

And the log say to me :

I wonder how I can understand better what my JML console says.
Here apparently getMylist().size() return 8945 before the method and 8947 after.
In there a way to display in the log the value of "String a" it is used in the counter-example?
Another way to say it : is there a way to display object behind reference, here : by reference I mean REF!val!64 , REF!val!68 and also this one : _JML__tmp448 .

If there are other place / forums to exchange about openJML let me know.

Thanks a lot,

[davidcok]

No unfortunately there is not a way to display the content of objects and strings. The main difficulty with your specs for addStringInList is that \old(getMylist()) and getMylist() are the same. The reference that is the value of mylist does not change. What you want to demonstrate is that \old(getMylist().size()) + 1 == getMylist().size() But to prove that you will need to give some specs for getMylist(), such as //@ ensures \result == mylist; - David

…

On Jun 26, 2020, at 6:00 AM, GabrielHerry ***@***.*** ***@***.***> > wrote: Hello, My error is certainly obvious but behind that, I wonder how I can understand-interpret better the result of the JML-log & JML-Trace with OpenJML Eclipse plugin and z3_4_3. Here my code and JML-log : package jmltest; import java.util.ArrayList; public class ListTest { private final /*@ spec_public @*/ ArrayList<String> mylist; public /*@ pure @*/ ArrayList<String> getMylist() { return mylist;} public ListTest() { mylist = new ArrayList<String>();} //@ ensures \old(getMylist()).size() + 1 == getMylist().size() ; public void addStringInList(String a){ this.mylist.add(a); } } And the log say to me : <https://user-images.githubusercontent.com/60090134/85843927-40533000-b7a2-11ea-8b01-af151f690180.png> I wonder how I can understand better what my JML console says. Here apparently getMylist().size() return 8945 before the method and 8947 after. In there a way to display in the log the value of "String a" it is used in the counter-example? Another way to say it : is there a way to display object behind reference, here : by reference I mean REF!val!64 , REF!val!68 and also this one : _JML__tmp448 . If there are other place / forums to exchange about openJML let me know. Thanks a lot, — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#698>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABITDQC6MNLDWMWEFHJ6RBTRYRWTTANCNFSM4OJFU32Q>.

[davidcok]

To say a bit more about the log. — you can see that the trace says \old(getMylist()) and getMylist() might be different lists. Hence the sizes of them could be arbitrary different. They might be different lists because there is no spec for getMylist() that constrains the result. David

…

On Jun 26, 2020, at 5:50 PM, David Cok ***@***.***> wrote: No unfortunately there is not a way to display the content of objects and strings. The main difficulty with your specs for addStringInList is that \old(getMylist()) and getMylist() are the same. The reference that is the value of mylist does not change. What you want to demonstrate is that \old(getMylist().size()) + 1 == getMylist().size() But to prove that you will need to give some specs for getMylist(), such as //@ ensures \result == mylist; - David > On Jun 26, 2020, at 6:00 AM, GabrielHerry ***@***.*** ***@***.***> > wrote: > > > Hello, > > My error is certainly obvious but behind that, I wonder how I can understand-interpret better the result of the JML-log & JML-Trace with OpenJML Eclipse plugin and z3_4_3. > > Here my code and JML-log : > > package jmltest; import java.util.ArrayList; public class ListTest { private final /*@ spec_public @*/ ArrayList<String> mylist; public /*@ pure @*/ ArrayList<String> getMylist() { return mylist;} public ListTest() { mylist = new ArrayList<String>();} //@ ensures \old(getMylist()).size() + 1 == getMylist().size() ; public void addStringInList(String a){ this.mylist.add(a); } } > > And the log say to me : > <https://user-images.githubusercontent.com/60090134/85843927-40533000-b7a2-11ea-8b01-af151f690180.png> > I wonder how I can understand better what my JML console says. > Here apparently getMylist().size() return 8945 before the method and 8947 after. > In there a way to display in the log the value of "String a" it is used in the counter-example? > Another way to say it : is there a way to display object behind reference, here : by reference I mean REF!val!64 , REF!val!68 and also this one : _JML__tmp448 . > > If there are other place / forums to exchange about openJML let me know. > > Thanks a lot, > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub <#698>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABITDQC6MNLDWMWEFHJ6RBTRYRWTTANCNFSM4OJFU32Q>. >

[GabrielHerry]

Ok, that working,
thank you very much for these answers!