Whiley (programming language)

Whiley
Influenced by

Paradigm	Imperative, Functional
Designed by	David J. Pearce
First appeared	2009

Stable release	0.3.40 / May 28, 2016 (2016-05-28)
Typing discipline	Static, strong, safe, structural, flow-sensitive
License	BSD
Website	whiley.org
Java, C, Python, Rust

Whiley is a general purpose multi-paradigm, compiled language developed by David Pearce.^[1] 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.^[2] The first public release of Whiley was made in June, 2010.^[3]

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.^[4] The project was also supported between 2012 and 2014 by the Royal Society of New Zealand's Marsden Fund.^[5]

The Whiley compiler currently generates code for the Java virtual machine and can thus inter-operate with Java and other JVM based languages.

Overview

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:^[6]

A verifying compiler uses mathematical and logical reasoning to check the correctness of the programs that it compiles.
— Tony Hoare

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,^[7] Why3^[8] and Frama-C.

Most previous attempts to develop a verifying compiler focused on extending existing programming languages with constructs for writing specifications. For example, ESC/Java and the Java Modeling Language add annotations for specifying preconditions and postconditions to Java. Likewise, Spec# and Frama-C add similar constructs to the C# and C programming languages. However, these languages are known to contain numerous features which pose difficult or insurmountable problems for verification.^[9] In contrast, the Whiley language was designed from scratch in an effort to avoid common pitfalls and make verification more tractable.^[10]

Design

The syntax of Whiley follows the general appearance of imperative or object-oriented languages. Indentation syntax is chosen over the use of braces to delineate statement blocks, given a strong resemblance to Python. However, the imperative look of Whiley is somewhat misleading as the language core is Functional and Pure.

Whiley distinguishes a function (which is Pure) from a method (which may have side-effects). This distinction is necessary as it allows functions to be used in specifications. A familiar set of primitive data types is available including bool, int, arrays (e.g. int[]) and records (e.g. {int x, int y). However, unlike most programming languages the integer data type, int, is unbounded and does not correspond to a fixed-width representation such as 32-bit two's complement. Thus, an unconstrained integer in Whiley can take on any possible integer value, subject to the memory constraints of the host environment. This choice simplifies verification, as reasoning about modulo arithmetic is a known and hard problem. Compound objects (e.g. arrays or records) are not references to values on the heap as they are in languages such as Java or C# but, instead, are immutable values.

Whiley takes an unusual approach to type checking referred to as "Flow Typing". In this scheme, variables can have different static types at different points in a function or method. Furthermore, on the true branch of a runtime type test, the variable being tested is retyped automatically (rather than requiring an explicit cast). Flow typing is similar to occurrence typing as found in Racket.^[11] To aid flow typing, Whiley supports union, intersection and negation types.^[12] Union types are comparable to sum types found in functional languages like Haskell but, in Whiley, they are not disjoint. Intersection and negation types are used in the context of flow typing to determine the type of a variable on the true and false branches of a runtime type test. For example, suppose a variable x of type T and a runtime type test x is S. On the true branch, the type of x becomes T & S whilst, on the false branch, it becomes T & !S. Whiley is also unusual in employing a structural rather than nominal type system. Modula-3, Go and Ceylon are examples of other languages which support structural typing in some form.

Whiley also supports reference lifetimes which are similar to those found in Rust. Lifetimes can be given when allocating new objects to indicate when they can be safely deallocated. References to such objects must then include lifetime identifier to prevent dangling references. Every method has an implicit lifetime referred to by this. A variable of type &this:T represents a reference to an object of type T which is deallocated with the enclosing method. Subtyping between lifetimes is determined by the outlives relation. Thus, &l1:T is a subtype of &l2:T if lifetime l1 statically outlives lifetime l2. A lifetime whose scope encloses another is said to outlive it. Lifetimes in Whiley differ from Rust in that they do not currently include a concept of ownership.

At the time of writing, Whiley has no built-in support for concurrency and no formal memory model to determine how reading/writing to shared mutable state should be interpreted.

Example

The following example illustrates many of the interesting features in Whiley, including the use of postconditions, loop invariants, type invariants, union types and flow typing. The function is intended to return the first index of an integer item in an array of integer items. If no such index exists, then null is returned.

 1 // Define the type of natural numbers
 2 type nat is (int x) where x >= 0
 3 
 4 public function indexOf(int[] items, int item) -> (int|null index)
 5 // If int returned, element at this position matches item
 6 ensures index is int ==> items[index] == item
 7 // If int returned, element at this position is first match
 8 ensures index is int ==> no { i in 0 .. index | items[i] == item }
 9 // If null returned, no element in items matches item
10 ensures index is null ==> no { i in 0 .. |items| | items[i] == item }:
11     //
12     nat i = 0
13     //
14     while i < |items|
15     // No element seen so far matches item
16     where no { j in 0 .. i | items[j] == item }:
17         //
18         if items[i] == item:
19             return i
20         i = i + 1
21     //
22     return null

In the above, the function's declared return type is given the union type int|null which indicates that either an int value is returned or null is returned. The function's postcondition is made of three ensures clauses, each of which describe different properties that must hold of the returned index. Flow typing is employed in these clauses through the runtime type test operator, is. For example, in the first ensures clause, the variable index is retyped from int|null to just int on the right-hand side of the implication operator (i.e. ==>).

The above example also illustrates the use of an inductive loop invariant. The loop invariant must be shown to hold on entry to the loop, for any given iteration of the loop and when the loop exits. In this case, the loop invariant states what is known about the elements of the items examined so far — namely, that none of them matches the given item. The loop invariant does not affect the meaning of the program and, in some sense, might be considered as unnecessary. However, the loop invariant is required to help the automated verifier using in the Whiley Compiler to prove this function meets its specification.

The above example also defines the type nat with an appropriate type invariant. This type is used to declare variable i and indicate that it can never hold a negative value. In this case, the declaration prevents the need for an additional loop invariant of the form where i >= 0 which would otherwise be necessary.

History

Whiley began in 2009 with the first public release, v0.2.27 following in June 2010 and v0.3.0 in September that year. The language has evolved slowly with numerous syntactical changes being made to-date. Versions prior v0.3.33 supported first-class string and char data types, but these were removed in favour of representing strings as constrained int[] arrays. Likewise, versions prior to v0.3.35 supported first-class set (e.g. {int}), dictionary (e.g. {int=>bool}) and resizeable list [int]), but these were dropped in favour of simple arrays (e.g. int[]). Perhaps most controversial was the removal of the real datatype in version v0.3.38. Many of these changes were motivated by a desire to simply the language and make compiler development more manageable.

Another important milestone in the evolution of Whiley came in version v0.3.40 with the inclusion of reference lifetimes, developed by Sebastian Schweizer as part of his Master's Thesis at the University of Kaiserslautern.

Influences

Whiley was one of the early pioneers of flow typing, a concept later picked up by other programming languages like Ceylon, TypeScript and the Facebook Flow.

References

This article is issued from Wikipedia - version of the 6/17/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.