Nested use of Quantifiers

Jan 6, 2013 at 12:17 AM

Does Spec# support nested use of quantifications.

If it does, can anyone please correct the example given below so that it gets compiled

(The postcondition i want to verify is given commented, but i cannot even get the uncommented one to compile)

public class C
{
int p11x,p11y,p12x,p12y,p21x,p21y,p22x,p22y;
public C(int p1,int p2,int p3,int p4,int p5,int p6,int p7,int p8)
{
    p11x=p1;
    p11y=p2;
    p12x=p3;
    p12y=p4;
    p21x=p5;
    p21y=p6;
    p22x=p7;
    p22y=p8;

    
 }
bool intersect()
ensures (result == true) ==> exists{ int x in (-100:100);{exists{int y in (-100:100); y==10};
//ensures (result == true) ==> exists{ int x in (-100:100);{exists{int y in (-100:100);{(y-p11y)*(p12x-p11x) -(p12y-p11y)*(x-p11x)==0 && (p11x <= x) && (x <= p12x) }}};
{
	int test1, test2;
	test1 = (( (p12x - p11x) * (p21y -p11y ))- ((p21x - p11x) * (p12y - p11y))) * (( (p12x - p11x) * (p22y -p11y ))- ((p22x - p11x) * (p12y - p11y)));
	test2 = (( (p22x - p21x) * (p11y -p21y ))- ((p11x - p21x) * (p22y - p21y))) * (( (p22x - p21x) * (p12y -p21y ))- ((p12x - p21x) * (p22y - p21y)));
	bool result =(test1 <= 0) && (test2 <= 0);
  return result;
}
}

Developer
Jan 13, 2013 at 2:26 PM

After fixing the curly braces in the postcondition to

    ensures (result == true) ==>
            exists{ int x in (-100:100); exists{int y in (-100:100); y==10}};

the code compiles on my Spec# installation (which I built from the sources). However, it throws an exception on rise4fun. We'll try to investigate why.

Both postconditions do not verify, which is due to the weak support for existential quantifiers.

    Peter

Jan 13, 2013 at 2:33 PM

Thanks