VCC for Spec# users

Jan 11, 2011 at 12:02 PM

Hello,

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) {

			_brake_force.increase(amount);

		}

	}




Regards,
Boris