Some interdisciplinary observations about getting the "right" specification

Abstract

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. © IFIP International Federation for Information Processing 2008.