Some Interdisciplinary Observations about Getting the 'Right' Specification

摘要

One can use formal approaches either post facto to try to show that a program has desirable properties or one can aim for verified by construction (VxC). The former approach tends to focus on specific properties such as avoiding the dereferencing of null pointers; the latter is more likely to address the question of whether the steps of design satisfy some overall specification. I not only prefer the latter but I have also argued that this is the main way to get formal methods to pay off: there is more mileage in getting a clean architecture than in trying to debug a bad design by retrofitting a proof.