|
|||||
|
The concept of effective union types in Whiley exposes some interesting features worth considering. In particular, they result in a separation between the readable and writeable view of a type. But, we’re getting ahead of ourselves! Let’s start with what exactly effective unions are… Effective Unions An effective union is a union type which . . . → Read More: Understanding Effective Unions in Whiley Recently, as part of our Programming Languages Reading group, we looked at the paper “Contracts in Practice” by Estler et al., (see here for a copy). This is quite an interesting paper and the authors perform an empirical investigation as to how contracts are used by programmers in practice. They dig out some data . . . → Read More: Program Specification in Practice? In this post, we’re going to consider representing the classic C string in Whiley. This turns out to be useful as we can then try to verify properties about functions which operate on C strings (e.g. strlen(), strcpy(), etc). If you’re not familiar with C strings, then the main points are: Roughly speaking, C . . . → Read More: Encoding C Strings in Whiley A couple of weeks back, I gave a presentation to the Wellington Java User Group. The talk provides a useful introduction to verifying software in Whiley, and shows a bunch of interesting examples. Anyway, you can see the presentation here: Wellington Java User Group Presentation from John Hurst on Vimeo. . . . → Read More: Verifying Software with Whiley Recently, I was listening to the latest edition of the Illegal Argument podcast, and it turns out they were discussing Whiley! (about 103:16 minutes in). The discussion was about how verification interacts with data from an untrusted source (e.g. from a database, network connection, etc). In particular, whether or not we can safely feed . . . → Read More: Verification with Data from Untrusted Sources Recently, I created a Whiley Cheat Sheet for use in our SWEN224 course and I thought it was useful enough to share! The goal of the cheat sheet is to provide some simple examples to help you get going, rather than provide a comprehensive reference. I tried to cram as much as I could . . . → Read More: Introducing the Whiley Cheat Sheet! In this article, I’ll look at some interesting issues relating to the use of break statements within loops, and how this affects the idea of a loop invariant. For some general background on writing loop invariants in Whiley, see my previous post. To recap the main points, here’s a simple function which requires a . . . → Read More: Loop invariants and Break Statements As the Whiley system is taking better shape every day, I’m starting to play around more and discover things. In particular, there are some surprising issues surrounding while loops and their loop invariants. These are things which I’ll need to work on in the future if Whiley is to stand any chance of being . . . → Read More: Thoughts on Writing Loop Invariants 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 |
 |
||||
|
Copyright © 2017 David J. Pearce - All Rights Reserved 61 queries. 0.391 seconds. |
|||||
