On Sunday, January 11, 2015, Michael Hutchinson <mhu...@xamarin.com> wrote:
> On 9 January 2015 at 16:32, Greg Young <gregoryyou...@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
_______________________________________________ Mono-devel-list mailing list Mono-devel-list@lists.ximian.com http://lists.ximian.com/mailman/listinfo/mono-devel-list
