Hi,

I am using DateTime objects in the invariants of a class; they pass the verification but when I build the project the following errors and other similar errors pops up with no location specified for them.

Error 1 The member 'System.DateTime.op_LessThan' must be pure, confined or state independent (use custom attributes Contracts.Pure and Contracts.Reads).

Error 2 The member 'System.DateTime.op_Equality' must be pure, confined or state independent (use custom attributes Contracts.Pure and Contracts.Reads).

Error 4 Static methods must be StateIndependent in invariants and model-field satisfies clauses.

My question is how I can fix these errors and still use DataTime type? The following code describes how I am using DateTime:

private DateTime departureTime;
private DateTime arrivalTime;

invariant departureTime < arrivalTime;

invariant (arrivalTime.Year == departureTime.Year && arrivalTime.Month == departureTime.Month && arrivalTime.Day == departureTime.Day && arrivalTime.Hour == departureTime.Hour) ==> (arrivalTime.Minute - departureTime.Minute > 20);

invariant (arrivalTime.Year == departureTime.Year && arrivalTime.Month == departureTime.Month && arrivalTime.Day == departureTime.Day && (arrivalTime.Hour - departureTime.Hour == 1)) ==> (arrivalTime.Minute <= 50 && departureTime.Minute >= 10);

Invariant DateTime.Now > arrivalTime ==> this.flightStatus == FlightStatus.Idle;

invariant DateTime.Now < departureTime ==> this.flightStatus == FlightStatus.Idle;

Thanks,

Adnan

Hi Adnan,

The Spec# compiler contains so-called out-of-band contracts for many types of the .NET API. These contracts also include purity annotation. So far, we have added out-of-band contracts mostly on demand; therefore, they are rather incomplete. I just tried to add the necessary annotations to DateTime, but without any success. I will try to figure out why it does not work, I supposed it is because DateTime is a struct, and Spec#'s support for structs has always been rather weak.

   Peter

Thanks

Hi Adnan,

I've just committed a fix for this. Please let me know if that doesn't do the trick.

Best regards,

Valentin

Excellent, It's working now.

Thanks,

Adnan

Hi,

Unfortunately the same problem returned back, I don't know what happened but I did not change any thing in my code.

Thanks,

Adnan