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
Recently, I was having a somewhat heated discussion with a friend about the Java I/O library (specificially java.io.*). His position was that the library is unnecessarily cluttered and verbose, and that I/O in C is much simpler and more productive. Whilst I agreed with some of that, I also argued that the Java I/O . . . → Read More: Comparing I/O in C with Java