Semantic Guidance and Feedback for the Construction of Specifications and Implementations

TL;DR

This paper introduces a method and tool for constructing and verifying specifications and implementations using use cases, with semantic feedback and algorithms to ensure accuracy, demonstrated through examples like linear search and text justification.

Contribution

It presents a novel approach to specification construction and verification using semantic feedback from use cases, including algorithms for accuracy checking and iterative refinement.

Findings

Effective specification accuracy verification algorithms

Incremental specification construction guided by semantic feedback

Successful application to linear search and text justification examples

Abstract

The problem of writing a specification which accurately reflects the intent of the developer has long been recognized as fundamental. We propose a method and a supporting tool to write and check a specification and an implementation using a set of use cases, \ie input-output pairs that the developer supplies. These are instances of both good (correct) and bad (incorrect) behavior. We assume that the use cases are accurate, as it is easier to generate use cases than to write an accurate specification. We incrementally construct a specification (precondition and postcondition) based on semantic feedback generated from these use cases. We check the accuracy of the constructed specification using two proposed algorithms. The first algorithm checks the accuracy of the specification against an automatically generated specification from a supplied finite domain of use cases. The second checks the accuracy of the specification via reducing its domain to a finite yet equally satisfiable domain if possible. When the specification is mature, we start to also construct a program that satisfies the specification. However, our method makes provision for the continued modification of the specification, if needed. We illustrate our method with two examples; linear search and text justify.