VCC for Spec# users

Jan 11, 2011 at 12:02 PM


I'm familiar with the Spec# terminology and I've noticed that some notations differ in VCC. For example, "valid" in Spec# means "object invariant holds", "consistent" means "mutable and owner is valid". A precondition for a method call is that the object is consistent. To establish this, the caller uses expose-environments.

Do equivalent notations, concepts, elements of the spec language in VCC exist in VCC an how are they called?

For example, how does [Rep] and expose(this) {...} in the following code snipped have to be translated?


 	[Rep] Range _brake_force = new Range();

	public void brake(long amount)

	requires 0 < amount;

	ensures active();


		expose(this) {