Invariants Cant access Constructor arguments?

[yu wen ng]

hi,

I am trying to add a Invariant as follow for my class, but it does not seems to read the variable that is provided as an argument?

Does this not work for cofoja's invariant?

@Invariant({ "_numbers!=null", "_numbers==numbers" })

public class Sorter {

private ArrayList<Integer> _numbers;

    public Sorter(ArrayList<Integer> numbers) {

        _numbers = numbers;

    }

....

}

Error 

error in contract: com.google.java.contract://com.google.java.contract/integerSort/Sorter.java:24: cannot find symbol

symbol  : variable numbers

location: class integerSort.Sorter

clause: _numbers==numbers

                  ^

[Nhat Minh Lê]

Hi,

No, indeed it can't. Invariants are checked for every external method
invaocations, not just the constructors, so there's no reason it would
have access to a specific constructor's parameters. Besides, that
wouldn't be consistent if you had multiple constructors, for example.

If you want to test that your constructor actually returns a correctly
initialized object, you should do that in the postcondition of the
constructor, not in the invariant. But _numbers != null can definitely
stay there.

Hope that helps,
Nhat

> --
> You received this message because you are subscribed to the Google Groups
> "cofoja" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to cofoja+un...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[yu wen ng]

Hi ,

Thanks for your reply.  As you have suggested it should be a postcondition stated on the constructor. 

My purpose to have it as an invariant ensure that _numbers consistenty assigned to numbers array pass by the constructor. 

This is to ensure that in between the methods/ codes that uses _numbers will ensure that the its referring to the same initalized objects and not referencing to others after its being called in another method. 

Therefore theres no way to do this?

I have two questions regarding about cofoja's invariants.

Firstly, you mention that " Invariants are checked for every external method invaocations", does that mean if the class itself calls its own methods, invariants will not be checked? 

For example A below, the sortArray method is called, will the Invariant be checked?

Secondly  is regarding about the semantic of the invariant, does the invariant check before and after the method is invoked, or just only after?

Example A

@Invariant({ "_numbers!=null"})

public class Sorter {

 private ArrayList<Integer> _numbers;

    public Sorter(ArrayList<Integer> numbers) {

        _numbers = numbers;

                sortArray(_numbers);

    }

            private sortArray(ArrayList<Integer> numbers) {

Collections.sort(_numbers);

        

    }

....

}

Sorry for all the inconvenince

Regards,

yu wen

[Nhat Minh Lê]

Hi,

On Sun, Jul 21, 2013 at 3:45 PM, yu wen ng <yu.w...@gmail.com> wrote:
>> Hi ,
>
>
> Thanks for your reply. As you have suggested it should be a postcondition
> stated on the constructor.
>
> My purpose to have it as an invariant ensure that _numbers consistenty
> assigned to numbers array pass by the constructor.
> This is to ensure that in between the methods/ codes that uses _numbers will
> ensure that the its referring to the same initalized objects and not
> referencing to others after its being called in another method.
> Therefore theres no way to do this?

No, if I understand correctly, there is no way to do that. The numbers
parameter is local to your constructor, after the call it disappears
and there's no way to refer to that afterwards (including in
invariants).

>
> I have two questions regarding about cofoja's invariants.
> Firstly, you mention that " Invariants are checked for every external method
> invaocations", does that mean if the class itself calls its own methods,
> invariants will not be checked?
> For example A below, the sortArray method is called, will the Invariant be
> checked?

No, the invariant won't be checked for sortArray(). This is so helper
methods can work on the internal member variables, temporarily leaving
them in an inconsistent state.

>
> Secondly is regarding about the semantic of the invariant, does the
> invariant check before and after the method is invoked, or just only after?

Both before and after.

Hope that helps,
Nhat

>
> Example A
>
> @Invariant({ "_numbers!=null"})
>
> public class Sorter {
>
> private ArrayList<Integer> _numbers;
>
>
> public Sorter(ArrayList<Integer> numbers) {
>
> _numbers = numbers;
>
> sortArray(_numbers);
>
> }
>
>
> private sortArray(ArrayList<Integer> numbers) {
>
> Collections.sort(_numbers);
>
>
>
> }
>
> ....
>
> }
>
>
>
> Sorry for all the inconvenince
>
>
> Regards,
>
> yu wen
>
>

[yu wen ng]

Hi,

Thank for your reply. As i am currently working on a school project and trying write a new annotation as an add on.

It somehow works like an Invariant indicated for the constructor and i need some help to start with.

Any idea what are the classes that i shall look into ?

Regards,

yu wen