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
>
>