Why do I need a witness clause when I define a subset type or newtype?
Why do I need a witness clause in subtype definitions like
type A = s: int | Prime(x) witness 13
Dafny generally assumes that types are non-empty; the witness is an example value that is in the type, demonstrating that the type is non-empty.
There are defaults for the
witness clause, so you don’t always have to have one. The default value is some zero-equivalent value:
int based types,
empty sets, sequence and maps for those base types.
And, it is permitted to have possibly empty types by using a witness clause
witness *, but there are restrictions on the use of possibly empty types.
For instance, a declaration of a variable with a possibly-empty type will need an initializer,
if that variable is ever used, because Dafny requires variables to be ‘definitely assigned’ before being used.
The Reference Manual contains a discussion about witness clauses.