34923
submission
Coryoth writes:
This first major release of EiffelStudio since it went GPL, and includes many improvements, including an overhaul of the look and feel. Versions are available for Windows, Linux, FreeBSD, OpenBSD, and Solaris, and provisionally for MacOS X. EiffelStudio provides an IDE, core libraries, and compiler for Eiffel — a language well worth a second look.
28074
submission
Coryoth writes:
In a UK government commissioned report by respected economist Sir Nicholas Stern concludes that mitigating global warming could cost around 1% of global GDP if spent immediately, but ignoring the problem could cost between 5% and 20% of global GDP. This 700 page report represents the first major report on climate change from an economist rather than a scientist. The report calls for, among other things, the introduction of green taxes and carbon trading schemes as soon as possible, and calls on the international community to sign a new pact on greenhouse emissions by next year rather than in 2010/11. At the very least the UK government is taking the report seriously, with both major parties proposing new green taxes. Stern points out, however, that any action will only be effective if truly global.
28064
submission
Coryoth writes:
The release of a report commisioned by the UK government by respected economist Sir Nicholas Stern has conluded that attempting to address anthropogenic global warming could cost around 1% of global GDP, if spent immediately, however ignoring the issue could end up costing between 5% and 20% of global GDP. The 700 page report is the first major report on climate change from an economist rather than a scientist. The report urges green taxes and carbon trading schemes to be put in place as soon as possible and also calls for the international community to sign a new pact on greenhouse emissions by next year rather than in 2010/11. At the very least the UK government is taking the report very seriously, and can be expected to take many of the actions described — both major parties are already proposing various green taxes in light of the report.
11101
submission
Coryoth writes:
Using automated theorem provers to verify code has generally been impractical for all but the most safety critical software projects. Both software and hardware have improved significantly. The quality and efficiency of modern automated theorem provers, such as ESC/Java2 and Spec#, have reached the point where they can be effectively integrated alongside unit tests to provide more complete coverage for test driven design and similar approaches. Recent research papers have speculated that such integration could be highly beneficial and is almost inevitable. Could it be that theorem proving could finally become an integral part of software development?
10945
submission
Coryoth writes:
Agile development and formal methods have generally been considered to be poles apart as far as software development methodologies go. It turns out that this may be far from true. Specification Driven Development(PDF) is an elegant marriage of Agile Test Driven Development with contract programming and lightweight formal methods. With high quality, fast, automated theorem provers making their way into the development world such as ESC/Java2 for Java, Spec# for C#, and ESpec for Eiffel, lightweight formal methods can be integrated into the Agile process. Espec provides an integrated system of Fit acceptance testing, unit testing, and theorem proving. Are similar integrated Agile specification based frameworks using JML and Spec# on the horizon for Java and C#?
10939
submission
Coryoth writes:
Traditionally if you want to write an avionics system for NASA you use formal methods and theorem provers at great expense, and if you want to write a business application you use an agile methodology and unit tests for a rapid feedback cycle. More recently, however, these seemingly incompatible approaches are coming together (PDF). The ESpec research project has put together an experimental system for Eiffel that, by extending unit tests with contracts, allows theorem proving to be integrated into an agile TDD system. ESpec provides a framework and tool suite that brings FIT acceptance testing, unit testing, design by contract, and theorem proving into a single environment with integrated reporting and fast turnaround. Given that more mature theorem provers already exist in ESC/Java2 for Java and Spec# for C#, surely it's only a matter of time before similar integrated systems appear for more popular languages.
10923
submission
Coryoth writes:
Agile development methods may soon incorporate automated theorem provers for code verification. The quality and efficiency of automated theorem provers for verifying code, such as ESC/Java2 and Spec#, have reached the point where they can be effectively integrated alongside unit tests in Agile methodology. Recent research papers have speculated that such integration could be highly beneficial and is almost inevitable. Could it be that theorem proving could become an integral part of Agile software development?
10809
submission
Coryoth writes:
Agile development and formal methods have generally been considered to be poles apart as far as software development methodologies go. It turns out that this is far from the case. Specification Driven Development(PDF) is an elegant marriage of Agile Test Driven Development with contract programming and lightweight formal methods. With high quality, fast, automated theorem provers making their way into the development world such as ESC/Java2 for Java, Spec# for C#, and ESpec for Eiffel, lightweight formal methods can be integrated into the Agile process. Espec provides an integrated system of Fit acceptance testing, unit testing, and theorem proving. Are similar integrated Agile specification based frameworks using JML and Spec# on the horizon for Java and C#?
9191
submission
Coryoth writes:
How do you convince co-workers of the benefits of extended static and runtime checking via contracts, and more detailed interface specification? Despite understanding the benefits static typing can provide for suitable projects, explaining the benefits of going one step further in specifying interfaces is proving difficult. Despite pragmatic systems like JML and Spec# which allow as much or as little extra specification as you need and still provide tangible benefits; despite automated theorem prover based systems, like ESC/Java2 and the Spec# verifier, which can do extensive checking statically and even produce potential counterexamples; fans of static type systems just don't seem to be able to see that their arguments for static rather than dynamic types apply equally well to contracts over static types alone. So what's the key to getting such people to consider stronger static checking?
7691
submission
Coryoth writes:
Literate Programs provides a growing wiki repository of well documented code. Articles are in literate programming style: a detailed plain english description of an algorithm with code samples interspersed. A click of the Download Code button will extract the code from the verbose documentation and provide you with straight code for you to play with. It's a repository of well documented algorithms complete with sample code; it's a repository to show off the style and functionality of a myriad of different programming languages (; It's a library of MIT licensed code for all your needs.
