### Question:

This example

// dafny Example.dfy
class A {
var x: string
}

type AA = a: A | a.x == "" witness * reads a



generates this error:

FAQReadsClause.dfy(6,37): Error: this symbol not expected in Dafny
1 parse errors detected in FAQReadsClause.dfy



but there is no obvious place to put a reads clause.

There is no place for the reads clause because no such clause should be needed. A type definition is not allowed to depend on a mutable field; the predicate in the subset type must be pure.

The general idiom is to add a predicate, often named Valid(), to a class that reads its fields and returns true if the class members are appropriately consistent. Then call Valid() in the pre- and post-conditions of methods and in preconditions of functions and predicates. Here is an example:

class A {
var x: string
var y: string
|x| == |y|
}
}

method Test(a: A)
requires a.Valid()
requires a.x == ""
modifies a
ensures a.Valid()
{
assert a.Valid(); // That's correct thanks to the precondition.
a.x := "abc"; // Because |a.y| == 0, we broke the Valid() predicate
assert !a.Valid(); // But that's ok.
a.y := "bca";
assert a.Valid(); // Now Dafny can prove this
// The postcondition holds
}


The {:autocontracts} attribute can be helpful here.

Note that the idiom using Valid() above is similar to the use of class invariants in other specification languages.