|
|||||
|
Proving that a loop always terminates is a common requirement when verifying software. The usual approach to doing this is to provide a loop variant function. This is typically an integer expression which decreases on every iteration of the loop. Consider the following loop: function contains([int] items, int item) => bool: int i = . . . → Read More: Loop Variant Relations The Whiley language takes an unusual approaching to static typing called flow typing. This helps to give Whiley the look-and-feel of a dynamically typed language. The key idea behind flow typing is to allow variables to have different types at different points in a program. For example, consider the following code written in a . . . → Read More: Formalising Flow Typing with Union, Intersection and Negation Types The Whiley language splits into a fully functional “core” and an imperative “outer layer”. References and objects do not exist within the functional core. However, they can exist within the imperative outer layer and are necessary for supporting state and other side-effecting computation. Here’s a simple example: define Buffer as ref { [int] items . . . → Read More: Flow Typing for References in Whiley An interesting and intuitive way of thinking about a type system is using a semantic interpretation. Typically, a set-theoretic model is used where a type T is a subtype of S iff every element in the set described by T is in the set described by S. The Semantic Model The starting point is . . . → Read More: A Semantic Interpretation of Types in Whiley I’ve been working hard over the last few weeks on the next release of Whiley, which should be out soon. However, I’ve got myself into a little bit of a pickle over the type system (again). I want the type system to be simple and easy to use, but at the same time efficient . . . → Read More: On the Duality of Types: the Ideals versus the Reals Recently, I came across an interesting problem with the type system I’m using in Whiley. Specifically, the problem relates to recursive types which are equivalent but not identical. Consider, for example, the following Whiley code: define Link as { int data, LinkedList next } define LinkedList as null | Link This is a fairly . . . → Read More: Normalising Recursive Data Types |
 |
||||
|
Copyright © 2022 David J. Pearce - All Rights Reserved 53 queries. 0.337 seconds. |
|||||
