|
|||||
|
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 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! 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! 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 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 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 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 |
 |
||||
|
Copyright © 2021 David J. Pearce - All Rights Reserved 49 queries. 0.320 seconds. |
|||||
