Expansion Contract.Ensures cens Emits a 'ensures' clause Jonathan de Halleux
System.Diagnostics.Contracts condition boolean invariant condition false condition