[Mono-dev] CodeContacts open sourced

[Greg Young]

On Sunday, January 11, 2015, Michael Hutchinson <mhutch at xamarin.com> wrote:

> On 9 January 2015 at 16:32, Greg Young <gregoryyoung1 at gmail.com
> <javascript:;>> wrote:
> > It's not source analysis it theorem proving think formal proving a la
> eiffel
>
> The Code Contracts tools analyze (and rewrite) compiled code, but
> there's no reason why equivalent source analysis tools couldn't use a
> theorem prover.


This is true it can work on any ast as of now it works on il. Previously it
worked wih output from spec# and was called boogie.

>
> > It's a massive!!!  task (like 5-10 man years) to bring it in as you need
> to
> > put contracts on all of the mono code
> >
> > This is part of why it has not done well for Microsoft is much of the
> > framework lacks co tracts which makes the theorem prover very difficult
> to
> > use (needs tons of assume clauses)
>
> The repo includes the contract annotations for the BCL, and we have
> the reference source for much of the BCL too.


Many of these are auto generated not manually written. They wrote a tool in
msr to try to extract them. This also brings up an interesting question if
mono intends to match every contract. It is also a higher level of coupling.

If I even use just a few libraries without contracts the contract prover is
very annoying to use think about a call stack

Call: check preconditions-> post conditions -> returns v1
Call: no contracts param v1 returns v2 ->
Call param v2 (how do you check preconditions?)

This gets worse when mutations are involved.

A big part of the reason the contracts library has not taken off is that
huge portions of library code in the space doesn't have contracts
associated with them. Also given the massive amounts of mutations that are
happening good contracts are often hard to write. A good example of this
would be stream.position post conditions after operations on a stream. Why
it's a particularly nasty example is that much of the contract is relying
on lower level code and assumes.

Don't get me wrong I love the idea of contracts. I am just pointing out
that it's a massive amount of work to get contracts on vast portions of
monos code base. If it's not pervasive then no one will use the contract
proving as its really annoying.

Cheers,

Greg



> - m
>


-- 
Studying for the Turing test
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ximian.com/pipermail/mono-devel-list/attachments/20150111/0e78568e/attachment.html>