Seamless Requirements

TL;DR

Seamless Requirements introduces a new approach for specifying functional requirements that enhances developer understanding and software quality while simplifying the process by eliminating the need for tests through formal verification.

Contribution

It presents a novel requirements specification method that improves clarity and consistency, reducing the need for translation and testing, applicable across various development models.

Findings

Improves developer understanding of requirements

Enhances software quality through formal verification

Simplifies development process by removing testing steps

Abstract

Popular notations for functional requirements specifications frequently ignore developers' needs, target specific development models, or require translation of requirements into tests for verification; the results can give out-of-sync or downright incompatible artifacts. Seamless Requirements, a new approach to specifying functional requirements, contributes to developers' understanding of requirements and to software quality regardless of the process, while the process itself becomes lighter due to the absence of tests in the presence of formal verification. A development case illustrates these benefits, and a discussion compares seamless requirements to other approaches.

Full text

1 Introduction

Seamless Requirements is a technique to close the various gaps that have long plagued the practice of software requirements:

• •

The gap between customers and developers (Section 1.1).

• •

The gap between agile and formal development (Section 1.2).

• •

The gap between construction and verification (Section 1.3).

To reach this goal, seamless requirements build on ideas coming from diverse sources, including literate programming [1], multirequirements [2], and formal verification [3]. A seamless requirement combines two elements: a contracted self-contained routine, which doubles as a proof obligation, and an associated natural language comment.

The approach assumes object-oriented non-concurrent setting and does not handle non-functional requirements.

1.1 Customers vs. Developers

By adding programming languages with contracts to the family of requirements specification notations, seamless requirements improve developers’ understanding of requirements that typically exist in some declarative form that has nothing to do with programming.

The modern taxonomy of requirements specification languages ([4, Chapter 4 “Requirements Specification and Documentation”]) provides a number of formal and semi-formal notations, and programming languages are not a part of this taxonomy. This implicitly isolates people (customers) who state requirements from people (developers) who implement them. As soon as the customers elicit and document requirements, demonstrate some “good” properties of the requirements within the chosen notation, the developers will have to map the notation into the semantics of the target programming language. Is there any way to check the translation at the same level of rigor used to derive those “good” properties of the requirements? Some approaches advocate modeling software at different angles using different notations to ensure its proper understanding by developers, but such an approach raises the problem of potential inconsistency between the views.

Seamless requirements express software functionality using the language best understood by developers: the programming language. The idea is not new [2], but its implementation is (Section 5.6 gives more details). A seamless requirement is a compilable contracted self-contained routine - specification driver [5] - equipped with a structured natural-language comment. The comment delivers the meaning of the requirement to the customers, and the program construct - to the developers. Specification drivers are expressive enough to fully capture algebraic specifications [5], and exercising their expressiveness is a driving force of the present research.

The idea of combining formal and natural language descriptions is present in goal-oriented requirements engineering [6], but the approach does not consider a programming language as a formal notation.

1.2 Agile vs. Formal Development

By nature both self-contained and formal, seamless requirements boost reliability of software produced using agile processes.

Compatibility of agile development and formal methods has long been a concern for software engineers ([7], [8]), particularly in the domain of mission and life-critical systems ([9], [10]). The studies have something in common: their main concern is integration of agile practices into development of software that has to be reliable and is currently developed using some conservative process. In the same time there is a lack of research that studies applicability of formal methods to agile development of not so critical mass-market software for increasing its reliability. This problem is among the concerns of the present article.

In agile development a functional requirement typically takes a form of a scenario describing user interaction with the to-be software. The scenario is then translated into a set of unit tests for ensuring functional correctness of the software with respect to the scenario. Scenarios and unit tests naturally fit the agile philosophy of frequently delivering software in small increments: they both are self-contained information units suitable for grouping into arbitrary sized sets. It is the very nature of tests that limits the level of formality in agile development: they exercise only a subset of the possible execution paths. Although there are scientific approaches for making a test suit cover the software well enough, agile methods do not consider tests as a very important artifact and do not advocate improving tests coverage too much.

Seamless requirements replace unit tests with specification drivers, testing with formal verification, and move structured natural language scenarios to comments on specification drivers. Specification drivers can capture scenarios in their abstract form (as opposed to unit tests), which is why it makes sense to conjoin them. The resulting requirement form keeps the fine granularity of tests and scenarios, while being mathematically formal.

1.3 Construction vs. Verification

Seamless requirements enable straightforward verification of existing software with respect to requirements without introduction of intermediate artifacts such as tests.

The modern software mass market rests on testing as the primary mechanism for checking functional correctness. Although tests are fundamentally imprecise (Section 1.2), there are scientific approaches to testing that enable production of test suits having reasonable code coverage with respect to some predefined criteria [11]. Such an approach may be suitable for greenfield software construction, but not always for verification of existing software that already works somehow. The problem is real: software quality cannot be higher than that of its least quality component. This means that, in order to reuse a third-party component, the development team has to make sure that its quality conforms to the quality standards defined in the project; in particular, it is necessary to generate sufficient number of tests and run them on the component. It is not surprising that such an effort is often considered as waste: why test something that is already on the market and works instead of putting more effort into construction?

Seamless requirements fix the issue by replacing testing with formal verification of specification drivers, which are formal and abstract representations of software usage scenarios. The only assumption upon which the approach rests is existence of a contract in the component, which is dictated by modularity of the verification approach[3].

2 Motivating Example

A simple example illustrates the idea of seamless requirements. The task is to implement a clock class that features seconds, minutes, hours, and days of week. The clock state should be updated through a special command called "tick" that advances the seconds counter. There is also an existing class CLOCK that does not feature the current day of week. The class is implemented and specified in Eiffel [12]. The implementation is closed: only a specification in the form of a contract is available. Figure 1 contains the visible part of the class. The frozen specifier prohibits inheriting from the CLOCK class and thus makes it usable only for instantiating and using its instances. It is also known that the hidden implementation of the tick command is provably correct with respect to its postcondition in Figure 1, and the correctness was established with the AutoProof verifier [3] for Eiffel programs with contracts.

2.1 Existing Code

This section takes a closer look at the visible parts of the CLOCK class in Figure 1. The space between the do and ensure keywords of the tick feature would typically contain executable instructions, which are hidden in this case. Logical assertions between the ensure and the closest end keyword constitute the postcondition of the feature. The postcondition logically connects the clock pre-state, which precedes any invocation of tick, with the post-state, which results from the invocation. The old keyword before some identifiers denotes values of the respective queries in pre-states. Accordingly, identifiers that go without the old keyword denote values of the respective queries in post-states.

Since it is not possible to modify the CLOCK class neither directly nor through inheritance, it seems reasonable in this context to implement the required extended class through the composition relation: in the new class declare a reference to an object of type CLOCK and reuse its functionality. In order to do so it is necessary to make sure that objects of the existing class, indeed, behave like a real clock. The extended clock development plan thus consists of the following major steps:

Identifying requirements to an extended clock. 2. 2.

Identifying requirements that are applicable to a non-extended clock. 3. 3.

Verifying the existing CLOCK class with respect to the requirements for a non-extended clock. 4. 4.

Reusing the existing class in the event of its successful verification. 5. 5.

Developing a completely new class otherwise.

2.2 Natural-language Requirements

Implementation of the first two steps of the plan starts with enumeration of the requirements in their natural-language form in Figure 2. Requirements (REQ1)-(REQ8) do not talk about the current day of week and thus are applicable to the existing implementation. Requirements (REQ9)-(REQ11) talk about the days counter and thus are applicable only to the extended implementation. For simplicity, days are represented with numbers from 0 to 6, where 0 corresponds to Monday, and 6 - to Sunday.

In many cases natural-language requirements are less clear and precise than the ones in Figure 2. This particular issue is irrelevant to the present work, which is why the example relies on the assumption that the natural-language requirements in the clock example are of high enough quality.

Step 3 of the plan from Section 2.1 is to check whether the CLOCK class meets requirements (REQ1)-(REQ8). This step, along with steps 4 and 5, is far less trivial than steps 1 and 2 and raises a number of questions.

2.3 Research Questions

2.3.1 RQ1

How to express precise semantics of the natural-language scenarios (REQ1)-(REQ8) using programming language constructs?

Natural-language statements in Figure 2 are comfortable for reading by human beings. This may be not enough, however, for those who will potentially implement the requirements. Natural language is a source of misinterpretations and ambiguities, which is why it is not enough to have requirements in this form [13]. What do statements (REQ1)-(REQ8) mean exactly in terms of the programming language abstractions? It would benefit the software developers to be able to precisely express the requirements in the programming language that will later be used for their implementation.

The question does not assume replacement of natural-language requirements with their programmatic counterparts: the goal is to have a representation which would encompass the both views with the possibility of extracting only one of them.

2.3.2 RQ2

How to make each requirement both self-contained and formal?

Requirements (REQ1)-(REQ11) are already self-contained and thus are suitable for agile development of arbitrary sized increments. How to enrich them with formality without sacrificing their granularity?

2.3.3 RQ3

How to understand whether the partially available implementation in Figure 1 meets requirements (REQ1)-(REQ8)?

It is possible to take requirements (REQ1)-(REQ11) and mentally convert them directly to a correct implementation, but the task assumes reuse of the existing class CLOCK in case of its correctness. How can one prove automatically that it meets requirements (REQ1)-(REQ8)? The only available part of the CLOCK class is its contract - in particular, the postcondition of command tick. It is also known that the hidden implementation of tick provably meets its postcondition. The question then reduces to the following one: how can one understand if the postcondition of tick meets requirements (REQ1)-(REQ8)?

3 Seamless Requirements

Figure 3 contains the (REQ1) requirement in the form of a seamless requirement - a contracted routine with a natural-language comment111Comments start with a double hyphen -- in Eiffel. The comment contains the natural-language representation of (REQ1) in Figure 2. The routine part, together with the signature and the contract parts, constitutes a proof obligation: "for any object clock of type CLOCK and any value current_second of type INTEGER, such that clock.second $<$ 59 and clock.second $=\,$ current_second, an execution of clock.tick results in clock.second $=\,$ current_second + 1". The modify (clock) clause in the precondition limits side effects of the tick routine: the routine is allowed to modify only the target object clock plus any object owned by clock [14]. It is possible to submit such a proof obligation to an automatic prover. AutoProof verifier fulfills this role for Eiffel programming language used in this example.

The idea to use non-operational routines with pre- and postconditions for complete specification of programs was first proposed in work [5]. The routines are assumed to be expressed only in terms of their formal arguments. That work introduces a new term "specification drivers" to denote such routines and shows that they are expressive enough to fully capture functional semantics of classes. Since specification drivers are, syntactically speaking, routines, it is possible to comment on them with natural-language statements - the ability to comment on routines is natural for any modern programming language. A seamless requirement consists of two important parts:

• •

Specification driver that captures the formal semantics for the requirement.

• •

Natural-language comment on the specification driver that informally captures the semantics.

A specification driver is a contracted routine expressed only in terms of its formal arguments and is understandable to AutoProof as a proof obligation.

The structure of a seamless requirement, together with the properties of specification drivers, answers the questions from Section 2.3 and ensures the core properties of seamless requirements, as the following sections illustrate.

3.1 RQ1: understandability to developers

Seamless requirements are contracted routines, which are programming language constructs understandable to programmers. Natural-language comments on these routines capture the informal representation of requirements that is understandable to customers. This duality makes a seamless requirement understandable to the two principal groups of stakeholders and semantically connects natural-language requirements to the CLOCK class, thus answering the RQ1 question from Section 2.3.1.

The idea of interweaving natural-language prose with programming language constructs was first proposed by Knuth in [1]. One of the theses of the present work is that it makes sense to use the standard commenting mechanism of the underlying programming language for this purpose.

3.2 RQ2: introducing formality into agile development

As their specification driver components are mathematically precise, seamless requirements do not accumulate ambiguity. Specification drivers are expressed completely in terms of their formal arguments, which is why they are also self-contained. The combination of the two properties benefits agile development with formality and does not interfere with its incrementality.

3.3 RQ3: utility for development activities

A seamless requirement is a natural-language statement and, at the same time, is a proof obligation. Consequently, to prove correctness of an implementation with respect to a natural-language requirement is to extend this requirement to the seamless form and then try to prove its proof obligation part. The approach also contributes to the following development activities.

3.3.1 Requirements documentation

A requirements document becomes an auxiliary class in the same namespace with the operational classes. Since seamless requirements are self-contained routines, there is no place for a naming conflict in the event of putting together multiple seamless requirements within a single class. Section 4.1 illustrates this concept on the clock example.

3.3.2 Specification validation

Seamless requirements, being proof-obligations understandable to AutoProof, introduce the notion of proving a requirement. Verification by AutoProof is modular: for example, for proving the req_1 requirement in Figure 3 AutoProof will use only the postcondition of the tick command. The modularity means that it is possible to verify a program with a hidden implementation with respect to a seamless requirement, when only a contract of the program is available. Section Section 4.2 illustrates the validation process for the existing CLOCK class.

3.3.3 Specification inference

It is possible to use seamless requirements for proof-driven development of programs from scratch. The automatic prover drives the process in this case. To infer a specification from a set of seamless requirements is to equip the operational classes with contracts strong enough to prove the requirements. Once the requirements pass verification by AutoProof, the development process switches to the implementation phase. To infer an implementation from a specification is to implement all the operational classes correctly with respect to their contracts [15]. The correctness is proved with the same verifier.