Common use of Syntax Clause in Contracts

Syntax. ‌ The syntax of the test specification language is given by a grammar as shown in Table 3.1. In general, the grammar of the test specification resembles that of the programming language given in Table 2.1 with small replacements and some extensions. To stress the extending character of the specification language the cutdecl ::= test class C; s ::= cutdecl T x; mokdecl { stmt } mokdecl ::= mock class C{C(T, . . . , T ); T m(T, . . . , T ); }; stmt ::= x = e | x = new C() | ε | stmt ; stmt | {T x; stmt } specification test unit class mock class statements | while (e) {stmt } | if (e) {stmt } else {stmt } stmtin ::= (C x)?m(T x).where(e) {T x; stmt ; !return e} | stmtin | stmtout | case { stmt in ; stmt } incoming stmt stmtout ::= e!m(e, . . . , e) {T x; stmt ; x =?return(T x).where(e) } | new(C x)?C(T x).where(e) {T x; stmt ; !return} outgoing stmt e ::= x | null | op(e, . . . , e) | new!C(e, . . . , e) {T x; stmt ; x =?return(T x).where(e) } expressions Table 3.1: Specification language for Japl: syntax extensions are highlighted in the grammar definition. Similar to the original defi- nition of a program p which consists of class import declarations, global variable definitions, class definitions, and a main body, the definition of a specification s consists of unit class declarations, global variable definitions, class declarations, and a specification body. In particular the class import declaration is replaced by the unit class declarations which also mention the names of the classes only. The class definition of a program is replaced by the mock class declaration where only the signature of the classes are specified. The method bodies are omitted since the specification body basically consists of the interaction trace and therefore implic- itly stipulates the behavior of the classes, rendering the method body definitions unnecessary. As the classes do not provide method bodies or field declarations it wouldn’t make sense to internally call their methods. Thus we omit the statements for (internal) method calls and field updates. For the same reason, the specifica- tion language only provides a simplified new construct which actually does not entail a constructor call but rather merely specifies the creation of a new object of a tester class. Furthermore, the specification language also provides sequential composition of statements, block statements, conditional statements, while loops, and the empty statement. Finally, the language allows for explicitly specifying the interaction sequence between the tester program and the unit under test. To this end, we introduce dedicated statement for each type of interaction as discussed previously. By introducing formal parameters in an incoming communication term we provided the possibility to relax a specification in terms of the expected incoming values. A case statement, where each branch consists of a sequence of statements which all start with an incoming call statement, enables a further relaxation with respect to the callee class and the called method or constructor, respectively: the tester’s environment (i.e. the unit under test) chooses a branch by provid- ing an incoming communication that matches the branch’s leading incoming call statement. Again, due to the lack of field declarations, we exclude field names from the set of possible expressions. Furthermore, due to the nested structure of the expec- tation specifications, the use of this would be ambiguous, hence is not supported. Instead, if we want to refer to the callee object of an incoming method call, we use the formal callee parameter of an incoming call term. Remark 3.2.1: Although the intention of the specification language is to describe the interface interaction between an object-oriented component and its environment by spec- ifying method calls, the specification language itself is not object-oriented. In particular, the language does not support the definition of (specification) classes but only the dec- laration of test class names and mock class signatures. An extension of the specification language with classes is discussed in Chapter 5.