Whiley (programming language)
 |
|
| Paradigm | Imperative, Functional |
|---|---|
| Designed by | David J. Pearce |
| First appeared | 2009 |
| Stable release |
0.3.40 / May 28, 2016
|
| Typing discipline | Static, strong, safe, structural, flow-sensitive |
| License | BSD |
| Website | whiley |
| Influenced by | |
| Java, C, Python, Rust | |
Whiley is a general purpose multi-paradigm, compiled language developed by David Pearce. The language combines features from the Functional and Imperative paradigms, is statically typed and supports formal specification through function preconditions, postconditions and loop invariants. The language is also notable for the use of flow-sensitive typing, also known as "flow typing".
The Whiley project began in 2009 in response to the "Verifying Compiler Grand Challenge" put forward by Tony Hoare in 2003. The first public release of Whiley was made in June, 2010.
Although Whiley is primarily developed by David Pearce, it is an open source project that has attracted contributions from a small community. The system has been used for a number of student research projects and also in teaching undergraduate classes. The project was also supported between 2012 and 2014 by the Royal Society of New Zealand's Marsden Fund.
The Whiley compiler currently generates code for the Java virtual machine and can thus inter-operate with Java and other JVM based languages.
The goal of Whiley is to provide a realistic programming language where verification is used routinely and without thought. The idea of such a tool has a long history, but was strongly promoted in the early 2000s through Hoare's Verifying Compiler Grand Challenge. The purpose of this challenge was to spur new efforts to develop a verifying compiler, roughly described as follows:
A verifying compiler uses mathematical and logical reasoning to check the correctness of the programs that it compiles.
The primary purpose of such a tool is to improve software quality by ensuring a program meets a formal specification. In other words, to help identify and eliminate software bug in the programs being developed. Whiley follows many attempts to develop such tools, including notable efforts such as SPARK/Ada, ESC/Java, Spec#, Dafny, Why3 and Frama-C.
...
Wikipedia