|
|||||
|
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 Recently, I encountered what I thought was a bug in the Whiley Compiler. The issue related to the current treatment of do/while loops and loop invariants. Having now spent a fair bit of time researching the issue, the answer is not so clear. The problem manifested itself when I tried to verify the following . . . → Read More: Loop Invariants and Do/While Statements An important component of the Whiley language is the use of recursive data types. Whilst these are similar to the algebraic data types found in languages like Haskell, they are also more powerful since Whiley employs a structural type system. So, what does all this mean? Well, let’s look at an example: define IntList as . . . → Read More: Iso-Recursive versus Equi-Recursive Types 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 My previous post on structural subtyping generated quite a few comments over on reddit. There were a lot of mixed opinions as to the pros and cons of having a [[structural type system]] instead of a [[Nominal typing|nominal type system]]. To help me digest and ponder it all, I thought I’d discuss the main . . . → Read More: The Case Against Structural Subtyping … ? Well, after an agonizing wait I finally heard the news that my paper on purity analysis was accepted to the Conference on Compiler Construction, 2011. Obviously, I’m stoked! The paper is: JPure: a Modular Purity System for Java. David J. Pearce. In Proceedings of the Conference on Compiler Construction, 2011. [PDF] A [[Pure function|pure . . . → Read More: Modular Purity Analysis for Java Modern programming languages generally use what is known as a [[Nominal typing|Nominal type system]]. This means types are associated with explicit names and subtyping relationships are explicit in the code (e.g. via extends or implements). This approach has the advantage of being relatively simple to implement; however, at the same time, it is quite . . . → Read More: Why not use Structural Subtyping? The idea behind flow-sensitive typing in Whiley is to give a statically typed language the look-and-feel of a [[Dynamic programming language|dynamically typed language]] (as much as possible). The following illustrates: int average([int] items): v = 0 for i in items: v = v + items[i] return v / |items| Here, we see that there . . . → Read More: More on Flow-Sensitive Typing The abstracts from the Dagstuhl seminar I recently attended are now available on the seminar site — there’s even a photo! The seminar was a lot of fun, and I encourage everyone who gets the chance to go along. The idea is that you get a bunch of people together, and then brainstorm for . . . → Read More: Whiley at Dagstuhl |
 |
||||
|
Copyright © 2021 David J. Pearce - All Rights Reserved 55 queries. 0.339 seconds. |
|||||
