Code Contracts and Third party code

Question

First of all, my compliments for the (probably) very hard work and the nice product you guys have developed. I think this will be the future of software developement.

Anyway, while trying to integrate code contracts into an existing code-base that makes use of an external ORM I got kind of stuck. Since I cannot change the code of the third party orm I gets quite hard to make the static checker usefull. For example the following code:

 

		using (UnitOfWork uow = new UnitOfWork())
			{
				try
				{
					Gast lvNewGast = new Gast(uow);
					Personalia lvPers = new Personalia(uow);
					Adres lvAddr = new Adres(uow);

					lvNewGast.Personalia = lvPers;
					lvNewGast.Woonadres = lvAddr;

					lvNewGast.Personalia.Achternaam = pvGuestSurName;
					lvNewGast.Woonadres.Straat = pvGuestStreetName;
					lvNewGast.Woonadres.Huisnummer = pvGuestHouseNumber;
					lvNewGast.Woonadres.Postcode = pvGuestZipCode;
					lvNewGast.Woonadres.Woonplaats = pvGuestCity;
					lvNewGast.Woonadres.Land = pvGuestCountry;
					uow.CommitChanges();
					Model.Gasten.Reload();
					return Model.Gasten.GastenCollection.Where(x => x.Oid == lvNewGast.Oid).First();
				}
				catch (Exception ex)
				{
					LoggerFactory.Instance.ErrorException("Error occured when creating a new guest", ex);
					throw;
				}
			}

As you can see, I create a new object here, set the values for the properties and save that object.
Then I reload my local cache and as a check to see if the object was really added i select the object from the local cache using the unique object id.
Now, we can be sure that this function shall never return null since First() will throw if Where() does not return exactly one object.

Now I got Contracts.Ensures(Contract.Result<T>() != null) but the theorem prover cant prove this (which is correct), but how can i fix it?

Answer 1

This will be hard to get past the static checker, even if we had contracts for the third party component. The main reason is that at the moment, the static checker does not really grok collections. We are working on that, but it's still some time out.

Whenever you need to work around the static checker, you can use Contract.Assume. In this case, you probably want to add something like the following:

  var result =  Model.Gasten.GastenCollection.Where(x => x.Oid == lvNewGast.Oid).First();
  Contract.Assume (result != null);
  return result;
}

---

Cheers, -MaF (Manuel Fahndrich)

Answer 2

[...]The main reason is that at the moment, the static checker does not really grok collections. We are working on that, but it's still some time out.

Do you have any idea of what time frame we're talking about? A week? A month? A year?

Static checking on collections would be very, very useful.

Answer 3

Thnx a lot for the answer!

 

However, the Assume is kind of a hacky way, but im afraid there is no other way. Like Jahn Otto said, do you have a timespan for the collections extension>?