Comments (5)
It looks like Dafny no longer allows quantifying over such possibly-heap types: trying this on the latest commit yields an error on the second line:
a quantifier involved in a predicate definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'x' (perhaps declare its type, 'T', as 'T(!new)')
Removing this line and the assert statement referencing it inside M3
does still allow the last assert to successfully verify, however.
from dafny.
Here are some further, related test cases:
class Basic {
var data: int
}
class Cell {
const x: int
var y: int
constructor (x: int, y: int)
decreases if x == y == 0 then 0 else 1
{
this.x, this.y := x, y;
if !(x == y == 0) {
var anotherCell := new Cell(0, 0);
}
}
}
method P0()
requires forall c: Basic :: c.data == 8
{
var o := new Basic;
o.data := 8;
assert forall c: Basic :: c.data == 8; // fine
}
method P1()
requires forall c: Basic :: c.data == 8
{
var o := new Basic;
assert forall c: Basic :: c.data == 8; // BOGUS: this should not verify -- may not hold for o
}
method Q()
requires forall c: Basic :: c.data == 8
{
var o := new object;
assert forall c: Basic :: c.data == 8; // BOGUS: this ought not verify (well, it could, but only if o is known not to be a Basic)
}
method M0()
requires forall c: Cell :: c.x == 8
{
var o := new Cell(7, 8);
assert forall c: Cell :: c.x == 8; // BOGUS: this should not verify -- does not hold for o (or for anotherCell)
}
method M1()
requires forall c: Cell :: c.x == 8
{
var o := new Cell(8, 8);
assert forall c: Cell :: c.x == 8; // BOGUS: this should not verify -- does not hold for anotherCell
}
method N0()
requires forall c: Cell :: c.y == 8
{
var o := new Cell(8, 7);
assert forall c: Cell :: c.y == 8; // error: does not hold for o (or for anotherCell)
}
method N1()
requires forall c: Cell :: c.y == 8
{
var o := new Cell(8, 8);
assert forall c: Cell :: c.y == 8; // error: does not hold for anotherCell
}
from dafny.
A note, mostly for myself: when we fix this, we need to make sure that the following still checks out:
method P1'()
requires forall c: Basic :: c.data == 8
{
var o := new Basic;
assert forall c: Basic :: c != o ==> c.data == 8;
}
from dafny.
I just had a look at the examples for quantifying, and I found a way to prove false, which summarizes well the challenge.
class Cell {
const x: int
constructor (x: int) ensures this.x == x {
this.x := x;
}
}
method M0()
requires forall c: Cell :: c.x == 8
{
var o := new Cell(7);
assert false;
}
Looking at the generated boogie code, I see that the precondition is encoded as:
requires (forall c#1: ref ::
{ _module.Cell.x(c#1) }
$Is(c#1, Tclass._module.Cell()) ==> _module.Cell.x(c#1) == LitInt(8));
This is wrong, because it does not depend on the heap at all.
The axiom should say that it's not true for all references, it's true for all the references that have already been allocated.
requires (forall c#1: ref ::
{ _module.Cell.x(c#1) }
$Is(c#1, Tclass._module.Cell()) && read($Heap, c#1, alloc) ==> _module.Cell.x(c#1) == LitInt(8));
Of @RustanLeino 's example, as of today, only P1, Q, M0, and M1 are problematic, the others are correctly handled.
However, fixing the axiom above would exactly fix P1, Q, M0 and M1.
And even if N0 and N1 could be proved, the fix above would still prevent them to verify.
from dafny.
One problem with the fix above is that, even if we replace 7 with 8, we still cannot prove anymore forall c: Cell :: c.x == 8
after the constructor. This is because we only know that what was allocated before is still allocated afterwards, but we don't know what new references were allocated in the heap.
Fortunately, we can fix that as usual by encoding it in the pre and post condition of the constructor (since, the constructor might allocate new references, it has to check locally that the predicate holds), but there is one caveat.)
class Cell {
const x: int
constructor (x: int)
requires forall c: Cell :: c.x == 8
decreases if x == 0 then 0 else 1
ensures this.x == x
ensures forall c: Cell :: c.x == 8 // Error, cannot prove this, unless we require x == 8 !
{
this.x := x;
if !(x == 0) {
var anotherCell := new Cell(0); // And if we require x =8, this fails. Yay!
}
}
}
method M0()
requires forall c: Cell :: c.x == 8
{
var o := new Cell(8);
assert forall c: Cell :: c.x == 8;
}
from dafny.
Related Issues (20)
- Dafny-to-Rust: SelectFn should produce a tree instead of a raw string
- Support for Rust tests
- Verifier crash on match within assert by within function
- `dafny run` crashes on `print @"\";` HOT 1
- Dafny server does not correctly show errors for postconditions of function
- --outer-module not tracked for empty parent modules
- Allow hiding subset types
- Opaque block
- Allow providing isolated proofs for the preconditions of function calls and operators
- Isolate all implicit assertions
- Improvement suggestions for the Dafny AST (AST.dfy) HOT 3
- Allow hiding ensures clauses
- Add a code action that automatically adds hide and reveal statements to a proof.
- Measure verification performance of Dafny integration test suite
- Parsing error for set comparison within array initialisation HOT 2
- Support for multiset update in rust HOT 1
- Support for trait's getter/setter in Rust HOT 1
- Shorthand syntax for partial application of functions
- Migration assistance for `--unicode-char`
- Support more efficient interop of target language strings with Dafny's string type HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from dafny.