Soundness of `calc` feature?

Nov 8, 2012 at 11:16 PM

I don't quite understand the `calc` feature. I can use it to ensure 'false':

ghost method CalcTest1(x: int, y: int)
  ensures x == 0;
{
	calc {
		x + y;
		{ assume x == 0; }
		y;
	}
	assert x == 0; // OK: follows from x + y == y;
}

ghost method CalcBad()
  ensures false;
{
  CalcTest1(1, 0);
  assert 1==0;
  assert false;
}

http://rise4fun.com/Dafny/PyfI

Am I missing something?

Nov 9, 2012 at 11:39 PM

Ah, nevermind. It just that assumptions are unsound.

ghost method CalcTest1(x: int, y: int)
  ensures x == 0;
{
  assume x == 0;
}

ghost method CalcBad()
  ensures false;
{
  CalcTest1(1, 0);
  assert 1==0;
  assert false;
}

http://rise4fun.com/Dafny/s3LBf