View source for Whiley (programming language)

{{Short description|None}}
{{Infobox programming language
| name = Whiley
| logo = 
| paradigm = [[Imperative programming|Imperative]], Functional
| released = June 2010
| designer = David J. Pearce
| latest release version = 0.6.1
| latest release date = {{Start date and age|2022|6|27}}
| typing = [[Type system#Strong and weak type systems|Strong]], [[Type safety|safe]], [[Structural type system|structural]], [[Flow-sensitive typing|flow-sensitive]]
| dialects = 
| implementations = 
| influenced by = [[Java (programming language)|Java]], [[C (programming language)|C]], [[Python (programming language)|Python]], [[Rust (programming language)|Rust]]
| license = BSD
| website = {{URL|whiley.org}}
}}

'''Whiley''' is an experimental programming language that combines features from the [[Functional programming|functional]] and [[Imperative programming|imperative]] paradigms, and supports [[Formal specification|formal specification]] through function preconditions, postconditions and [[Loop invariant|loop invariant]]s.<ref name=home>{{cite web|url=http://whiley.org/|title=Whiley Homepage}}</ref> The language uses [[Flow-sensitive typing|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 [[Biography:Tony Hoare|Tony Hoare]] in 2003.<ref>{{cite journal|title=The Verifying Compiler: A Grand Challenge for Computing Research | doi=10.1145/602382.602403 | volume=50 | journal=Journal of the ACM | pages=63–69| year=2003 | last1=Hoare | first1=Tony | s2cid=441648 }}</ref> The first public release of Whiley was in June, 2010.<ref>{{cite web|url=http://whiley.org/2010/06/24/whiley-v0-2-7-released/|title=Whiley v0.2.27 Released!}}</ref>

Primarily developed by David Pearce, Whiley is an open source project with contributions from a small community. The system has been used for student research projects and in teaching undergraduate classes.<ref>{{cite web|url=http://whiley.org/people/|title=whiley.org/people}}</ref>  It was supported between 2012 and 2014 by the Royal Society of New Zealand's Marsden Fund.<ref>{{cite web|url=http://www.royalsociety.org.nz/programmes/funds/marsden/ |title=Marsden Fund}}</ref>

The Whiley compiler generates code for the [[Java virtual machine]] and can interoperate with Java and other JVM-based languages.

== Overview ==

The goal of Whiley is to provide a realistic programming language where [[Formal verification|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 [[Biography:Tony Hoare|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:<ref>{{cite journal|title=The Verifying Compiler: A Grand Challenge for Computing Research | doi=10.1145/602382.602403 | volume=50 | journal=Journal of the ACM | pages=63–69| year=2003 | last1=Hoare | first1=Tony | s2cid=441648 }}</ref>

{{Quote|text=A  verifying  compiler  uses  mathematical  and  logical  reasoning  to  check  the correctness  of  the  programs  that  it  compiles.|author=Tony Hoare}}

The primary purpose of such a tool is to improve [[Software quality|software quality]] by ensuring a program meets a [[Formal specification|formal specification]]. Whiley follows many attempts to develop such tools, including notable efforts such as [[SPARK (programming language)|SPARK/Ada]], ESC/Java, Spec#, [[Dafny]], Why3,<ref>{{cite web|url=http://why3.lri.fr/|title=Why3 --- Where Programs Meet Provers}}</ref> and [[Software:Frama-C|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 (programming language)|Java]].  Likewise, Spec# and [[Software:Frama-C|Frama-C]] add similar constructs to the [[C Sharp (programming language)|C#]] and [[C (programming language)|C]] programming languages.  However, these languages are known to contain numerous features which pose difficult or insurmountable problems for verification.<ref>{{cite journal|title=Specification and verification: the Spec# experience | doi=10.1145/1953122.1953145 | volume=54 | issue=6 | journal=Communications of the ACM | page=81| year=2011 | last1=Barnett | first1=Mike | last2=Fähndrich | first2=Manuel | last3=Leino | first3=K. Rustan M. | last4=Müller | first4=Peter | last5=Schulte | first5=Wolfram | last6=Venter | first6=Herman | s2cid=29809 }}</ref> In contrast, the Whiley language was designed from scratch in an effort to avoid common pitfalls and make verification more tractable.<ref>{{cite journal|title=Designing a Verifying Compiler: Lessons Learned from Developing Whiley | doi=10.1016/j.scico.2015.09.006 | volume=113 | journal=Science of Computer Programming | pages=191–220| year=2015 | last1=Pearce | first1=David J. | last2=Groves | first2=Lindsay | doi-access=free }}</ref>

== Features ==

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 (programming language)|Python]].  However, the imperative look of Whiley is somewhat misleading as the language core is [[Functional programming|functional]] and [[Pure function|pure]].

Whiley distinguishes a <code>function</code> (which is [[Pure function|pure]]) from a <code>method</code> (which may have [[Side effect (computer science)|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 <code>bool</code>, <code>int</code>, arrays (e.g. <code>int[]</code>) and records (e.g. <code>{int x, int y}</code>).  However, unlike most programming languages the integer data type, <code>int</code>, is unbounded and does not correspond to a fixed-width representation such as 32-bit [[Two's complement|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 (programming language)|Java]] or [[C Sharp (programming language)|C#]] but, instead, are [[Immutable object|immutable]] values.

Whiley takes an unusual approach to type checking referred to as "Flow Typing." Variables can have different static types at different points in a function or method. Flow typing is similar to ''occurrence typing'' as found in [[Racket (programming language)|Racket]].<ref>{{cite web|url=https://docs.racket-lang.org/ts-guide/occurrence-typing.html|title=Occurrence Typing}}</ref>  To aid flow typing, Whiley supports [[Union type|union]], [[Intersection type|intersection]] and negation types.<ref>{{Cite web|url = http://homepages.ecs.vuw.ac.nz/~djp/files/VMCAI13.pdf|title = Sound and Complete Flow Typing with Unions, Intersections and Negations.|date = 2013|website = |publisher = |last = Pearce|first = David}}</ref>  Union types are comparable to [[Tagged union|sum types]] found in functional languages like [[Haskell (programming language)|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 <code>x</code> of type <code>T</code> and a runtime type test <code>x is S</code>.  On the true branch, the type of <code>x</code> becomes <code>T & S</code> whilst, on the false branch, it becomes <code>T & !S</code>.

Whiley uses a [[Structural type system|structural]] rather than nominal type system. [[Modula-3]], [[Go (programming language)|Go]] and [[Ceylon (programming language)|Ceylon]] are examples of other languages which support structural typing in some form.

Whiley supports ''reference lifetimes'' similar to those found in [[Rust (programming language)|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 pointer|dangling references]].  Every method has an implicit lifetime referred to by <code>this</code>.  A variable of type <code>&this:T</code> represents a reference to an object of type <code>T</code> which is deallocated with the enclosing method.  Subtyping between lifetimes is determined by the ''outlives'' relation.  Thus, <code>&l1:T</code> is a subtype of <code>&l2:T</code> if lifetime <code>l1</code> statically outlives lifetime <code>l2</code>.  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''.

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 <code>item</code> in an array of integer <code>items</code>.  If no such index exists, then <code>null</code> is returned.

<source lang="whiley">
// Define the type of natural numbers
type nat is (int x) where x >= 0

public function indexOf(int[] items, int item) -> (int|null index)
// If int returned, element at this position matches item
ensures index is int ==> items[index] == item
// If int returned, element at this position is first match
ensures index is int ==> no { i in 0 .. index | items[i] == item }
// If null returned, no element in items matches item
ensures index is null ==> no { i in 0 .. |items| | items[i] == item }:
    //
    nat i = 0
    //
    while i < |items|
    // No element seen so far matches item
    where no { j in 0 .. i | items[j] == item }:
        //
        if items[i] == item:
            return i
        i = i + 1
    //
    return null
</source>

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

The above example also illustrates the use of an inductive [[Loop invariant|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 <code>items</code> examined so far — namely, that none of them matches the given <code>item</code>.  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 <code>nat</code> with an appropriate [[Class invariant|type invariant]].  This type is used to declare variable <code>i</code> 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 <code>where i >= 0</code> which would otherwise be necessary.

== History ==

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

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

==References==
{{Reflist}}

[[Category:Academic programming languages]]
[[Category:Experimental programming languages]]
[[Category:High-level programming languages]]
[[Category:Free software projects]]

{{Sourceattribution|Whiley (programming language)}}