Some Interdisciplinary Observations about Getting the "Right" Specification (2008)

Author(s): Jones CB

    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.

    Notes: Volume contains revised selected papers and discussions from the conference.

      • Date: 10-13 October 2005
      • Conference Name: Verified Software: Theories, Tools, Experiments - First IFIP TC 2/WG 2.3 Conference (VSTTE 2005)
      • Volume: 4171
      • Pages: 64-69
      • Publisher: Springer
      • Publication type: Conference Proceedings (inc. abstract)
      • Bibliographic status: Published

      Professor Cliff Jones

      • Telephone: +44 191 208 8183