Re: [Mono-dev] CodeContacts open sourced
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
Re: [Mono-dev] CodeContacts open sourced
Regarding XS/MD support for the code contracts tools, there are really two pieces. The first is to port/reimplement the VS addin. It doesn't look particularly complex, a proof of concept might only take a couple of days. This would be glorious. They seem to be doing some kind of source-analysis like support, where they show potential problems. The second is figuring out how to build and ship the analysis tools, contract annotations and MSBuild tasks. AFAIK On Windows they're shipped in a MSI installer, but there are scripts to build a NuGet package too, though it doesn't seem to be on the public NuGet server. I think we could ship this with Mono itself (once we figure out how to build it). I tried to build it, but failed.Then again, I tried to build on Windows, and failed too :-) miguel ___ Mono-devel-list mailing list Mono-devel-list@lists.ximian.com http://lists.ximian.com/mailman/listinfo/mono-devel-list
Re: [Mono-dev] CodeContacts open sourced
See below. On Friday, January 9, 2015, Miguel de Icaza mig...@xamarin.com wrote: Regarding XS/MD support for the code contracts tools, there are really two pieces. The first is to port/reimplement the VS addin. It doesn't look particularly complex, a proof of concept might only take a couple of days. This would be glorious. They seem to be doing some kind of source-analysis like support, where they show potential problems. It's not source analysis it theorem proving think formal proving a la eiffel 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) Greg The second is figuring out how to build and ship the analysis tools, contract annotations and MSBuild tasks. AFAIK On Windows they're shipped in a MSI installer, but there are scripts to build a NuGet package too, though it doesn't seem to be on the public NuGet server. I think we could ship this with Mono itself (once we figure out how to build it). I tried to build it, but failed.Then again, I tried to build on Windows, and failed too :-) miguel -- 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
[Mono-dev] CodeContacts open sourced
Hey guys, Microsoft has open sourced their CodeContracts tools: https://github.com/CodeContractsDotNet/CodeContracts The companion class libraries are here: https://github.com/mono/referencesource/tree/mono/mscorlib/system/diagnostics/contracts While Mono has an implementation, it might be a good idea to replace them with the Microsoft version, in case the tools depend on some internal bits. In addition, it seems like we could enable MonoDevelop/XamarinStudio to support code contracts now. ___ Mono-devel-list mailing list Mono-devel-list@lists.ximian.com http://lists.ximian.com/mailman/listinfo/mono-devel-list
