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?
|
|||||
|
Flow-sensitive typing (a.k.a. “Flow Typing”) is definitely getting more popular these days. Ceylon, Kotlin, TypeScript, Racket, Whiley all support flow typing in some form. Then, of course, there’s Facebook Flow and the list goes on! Recently, I’ve made some fairly major updates to the internals of the Whiley compiler (basically, redesigning the intermediate language). . . . → Read More: Flow Typing with Constrained Types 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 We’ve started using Whiley again in my second year course Formal Foundations of Programming. The aim of this course is to introduce students into a range of techniques related to software correctness. So far, we’ve looked at some static analysis and model checking tools. Anyway, last week I gave an introductory lecture on writing . . . → Read More: Introductory Lecture on Verification in Whiley 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 Verification tools often support the use of ghost variables to help in the verification process. A ghost variable is not needed for the program to execute, and will not be compiled into object code. Typically, they are declared with a ghost modifier or similar, but are otherwise identical to normal program variables (i.e. they . . . → Read More: Understanding Ghost Variables in Software Verification 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 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 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 |
 |
||||
|
Copyright © 2021 David J. Pearce - All Rights Reserved 51 queries. 0.294 seconds. |
|||||
