Today, more then ever before, I/O dominates what software is about. Of course, it’s always been important but, with increasing bandwidths, I/O seems to be what most programs now spend most of their time doing. This leads to interesting questions about how, for example, to handle millions and millions of concurrent connections and we . . . → Read More: Input / Output and the Object-Oriented Paradigm
|
|||||
|
It is with some disappointment that I’ve finally decided to release v0.3.19 despite this being almost 3 months overdue! The disappointment arises because, despite a lot of valiant effort, verification is still not working very well — and, in fact, is probably worse than the previous release! However, on the other hand, I have . . . → Read More: Whiley v0.3.19 Released! 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 A surprisingly common question people ask me when I talk about compile-time checking of pre-/post-conditions and invariants is: how do you deal with I/O? To understand what the difficulty is, let’s consider a simple example in Whiley: define nat as int where $ >= 0 define pos as int where $ > 0 define . . . → Read More: Compile-Time Verification and I/O In this article, I’ll look at a common problem one encounters when verifying programs: namely, writing loop invariants. In short, a loop invariant is a property of the loop which: holds on entry to the loop; holds after the loop body is executed; holds when the loop finishes. Loop invariants can be tricky to . . . → Read More: Understanding Loop Invariants in Whiley I was having an interesting discussion with a colleague today about various aspects of Whiley, and we came up with an interesting bit of example code which is something of a puzzler. Consider these two different versions of a function f(any): Version 1: int f(any x): if x is string: return g(x) else: return . . . → Read More: Whiley Puzzler #1 The next version of Whiley is upon us! This consists of mostly lightweight improvements over v0.3.17 and various bug fixes (see issues for more). I have now been attempting to verify some of the microbenchmarks in Wybench, with some useful progress being made (although it is flushing out a lot of issues). ChangeLog Lots . . . → Read More: Whiley v0.3.18 Released! Today’s edition of the Dominion Post (Wellington’s Local Newspaper) features a nice article on Whiley:
Obviously, I’m very excited to see Whiley being talked about in our local newspaper, and I think the article does a nice job of it. There is also an electronic version as . . . → Read More: Whiley Features in the Dominion Post! Recently, I got hold of a Papilio One (which you can think of as the Arduino of FPGAs). The Papilio board has a Xilinx Spartan 3 on board, which is plenty enough to get started learning about FPGAs. Here’s what the board looks like:
Now, it might look big above … . . . → Read More: Testing out my Papilio FPGA! The Whiley programming language is about developing more reliable software and, of course, embedded systems is one of the biggest areas that could benefit. Obviously, then, we need an “embedded system” to test Whiley with, right? At least, that’s the thinking behind my recent endeavor to create an Arduino-based Robot. After some discussion with our workshop . . . → Read More: Building an Arduino Robot (for Testing Whiley) |
 |
||||
|
Copyright © 2013 David J. Pearce - All Rights Reserved 61 queries. 0.612 seconds. |
|||||
Popular Posts