Robust/src/Tests/ssJava/flowdown/test.java

   1 public class test{
   2     locdef{
   3         F<D,F<E,D<B,E<C,B<A,C<A,A<T,T<U
   4         //C<B,B<A,F<E,E<D,A<T,D<T
   5     }
   6
   7     @A int a;
   8     @B int b;
   9     @C int c;
  10     @D int d;
  11     @E int e;
  12     @T foo f;
  13     @T bar bar;
  14     @U foo u;
  15
  16     public static void main (String args[]){
  17         @T test t=new test();
  18         t.doit();
  19     }
  20
  21     public void doit(){
  22         //f=d+e;
  23
  24         @delta("LOC(d2result)") int d3result;
  25         @delta("D,FC") int result;
  26         @delta("LOC(result)") int d2result;
  27
  28         d3result=d2result+a;
  29
  30         //e=a+c;
  31
  32         //result = f.a + f.b; // glb(f.a,f.b)=[T,FB]
  33                             // then, compare LOC(result) and [T,FB]
  34
  35         //result=f.a+u.b;
  36
  37         //f.b=u.a; // u.a gives us a location: delta(U,FA)
  38                  // f.b is at least lower than delta(U,FA)
  39                  // by base comparison,
  40                  // if LOC(f)<LOC(u) & LOC(foo.b)<LOC(foo.a)
  41                  // then, it's okay
  42
  43         //bar.b=u.a; // u.a gives a new location: delta(U,FA)
  44                    // bar.b is at least lower than delta(U,FA)
  45                    // by base comparison
  46                    // if LOC(bar)<LOC(u)
  47                    // but no ordering relation between LOC(bar.b) and LOC(foo.a)
  48                    // is it okay to allow it?
  49                    // seems to be okay because there is no way to
  50                    // get it back to u.b or something else.
  51     }
  52 }
  53
  54 class foo{
  55
  56     locdef{
  57         FC<FB,FB<FA
  58     }
  59
  60     @FA int a;
  61     @FB int b;
  62     @FC int c;
  63
  64 }
  65
  66 class bar{
  67
  68     locdef{
  69         BC<BB,BB<BA
  70     }
  71
  72     @BA int a;
  73     @BB int b;
  74     @BC int c;
  75
  76 }