|
By Dave, on September 30th, 2010
With the recent addition of for and while loops to Whiley, I’ve been able to fiddle around with [[loop invariants]] and already I noticed a few things. Consider this little program:
// The current parser state define state as { string input, int pos } where pos >= 0 && pos <= |input| state . . . → Read More: Thoughts on Loop Invariants
By Dave, on September 29th, 2010
Well, after a significant amount of effort, many sleepless nights, and too many test cases going green, then red, then green, then red … it’s finally here!!!
In the process of moving from v0.2.X to v0.3.0, I have rewritten probably 75% of the code from scratch. The new version is working quite well, and . . . → Read More: Whiley v0.3.0 Released!
By Dave, on September 23rd, 2010
Finally, in the upcoming release of Whiley, I have added support for both while and for loops — which is about time. Here’s an example:
define nat as int where $ >= 0 nat sum([nat] list): r=0 i=0 while i < |list| where r >= 0: r = r + list[i] i = i . . . → Read More: Whiley gets a While Loop!
By Dave, on September 22nd, 2010
In the ensuing months since the previous release of Whiley, I have been working away on a major rewrite of the compiler. This is now almost ready, at last! One of the “executive decisions” I made recently, was to move away from a declared variable model to a completely [[Data-flow analysis|flow-sensitive]] typing model. To . . . → Read More: On Flow-Sensitive Types in Whiley
By Dave, on September 20th, 2010
Recently, Simon Doherty gave a short talk on using [[Java Pathfinder]] to find bugs in Java programs. Java Pathfinder is a model checker for Java code, particularly suited to reasoning about multi-threaded code and finding concurrency bugs. Roughly speaking, it searches through all of the different possible execution traces for a given piece of . . . → Read More: Java Pathfinder
By Dave, on September 19th, 2010
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
By Dave, on September 8th, 2010
I’ve just been watching this YouTube presentation by James Bach:
James has a very tongue-in-cheek style, which I rather like, and he’s obviously not a great fan of the academic establishment:
“Testing is not part of Computer Science. Computer Science likes to think that testing is part of Computer Science. But, if you . . . → Read More: James Bach on Software Testing
|
|