(How) Did you specify your test suite ?
Helmut Veith
Formal Methods in Systems Engineering
Vienna University of Technology
Joint work with
Andreas Holzer, Christian Schallhart, and Michael Tautschnig
high level model
synthesis / implementation
Proper semantics ?
high level programming language
compilation
Compiler errors.
Testing
executable
execution
hardware
Execution time.
Power consumption.
Processor bugs.
Production errors.
The purpose of abstraction is not to be vague, but to create a new semantic
level in which one can be absolutely precise.
Award Lecture]
We[Dijkstra,
are not Turing
there yet.
Software Testing
Software
Testing
Random Testing?
Directed Testing?
Manual Testing?
173
if (ctrl_io_in[SENS_IMPULS]) {
174
if (!lastImp){
175
if (ctrl_io_out[MOTOR_ON]) {
176
if (directionUp) {
177
++cnt;
178
} else {
179
--cnt;
180
}
181
}
182
else if (timImp>0) {
183
if (directionUp) {
184
++cnt;
185
} else {
186
--cnt;
187
}
188
}
189
}
190
}
191
if (ctrl_io_in[SENS_BOTTOM]) {
192
cnt = 0;
193
cntValid = TRUE;
194
}
195
lastImp = ctrl_io_in[SENS_IMPULS];
196
if (timImp>0) {
197
--timImp;
198
if (timImp==0) {
199
if (cmd!=CMD_NONE) {
200
cmd = CMD_NONE;
There is no201
general purpose
formalism for white box
}
202
}
test case specification
!
203
}
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Basic Block Coverage
Test suite such that each basic block is executed at least once
How did you specify your test suite ?
6
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
Decision Coverage
Conditional statements evaluate to true/false
How did you specify your test suite ?
7
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
Condition Coverage
Atomic conditions evaluate to true/false
How did you specify your test suite ?
8
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
Condition/Decision Coverage
Union of condition and decision coverage
How did you specify your test suite ?
9
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
a
if ((a || b) && c)
F
d = 0;
else
F
unimplemented();
F
return d*2;
F
}
T
b
c
F
F
F
T
T
F
T
T
F
F
T
F
T
T
T
F
T
T
T
Multiple Condition Coverage
All Boolean combinations of atomic conditions in complex conditions
How did you specify your test suite ?
10
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Def-Use Coverage
Cover all definition/use pairs of a variable d
How did you specify your test suite ?
11
New Coverage Criteria
1
2
3
4
5
6
7
8
9
10
11
12
13
void insert(int * a, int pos) {
...
}
int main(int argc, char * argv[]) {
int i;
int A[100];
for (i=0; i<100; ++i)
insert(A, i);
return 0;
}
Loop-Bounded Path Coverage
All paths through main and insert
Pass each statement two times
How did you specify your test suite ?
12
New Coverage Criteria
1 int partition(int a[], int left, int right) {
2
int v = a[right], i = left - 1, j = right, t;
3
for (;;) {
4
while (a[++i] < v) ;
5
while (j > left && a[--j] > v) ;
6
if (i >= j) break;
7
t = a[i]; a[i] = a[j]; a[j] = t;
8
}
9
t = a[i]; a[i] = a[right]; a[right] = t;
10 return i;
11 }
Cartesian Block Coverage
All pairs and triples of basic blocks in function partition
How did you specify your test suite ?
13
Specs for Working Programmers
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
Cover Specific Lines of Code
Lines 4 and 6
How did you specify your test suite ?
14
Specs for Working Programmers
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
void eval(int * a, int first, int last) {
if (first > last) return;
printf("a[%d]=%d\n", first, a[first]);
eval(a+1, first+1, last);
return;
}
int main(int argc, char * argv[]) {
int i;
int A[100];
for (i=0; i<100; ++i)
insert(A, i);
eval(A, 0, 100);
return 0;
}
Restricted Scope of Analysis
Basic block coverage in function eval only
How did you specify your test suite ?
15
Specs for Working Programmers
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
void sort(int * a, int len) {
int i, t;
for (i=1; i<len; ++i) {
if (compare(a[i-1], a[i])) continue;
t=a[i]; a[i]=a[i-1]; a[i-1]=t;
}
}
void eval(int * a, int len) {
int i;
for (i=0; i < 3; ++i)
printf("a[%d]=%d\n", i, a[i]);
}
int main(int argc, char * argv[]) {
int i; int A[100];
for (i=0; i < 100; ++i) sort(A, 100);
eval(A, 100);
return 0;
}
Interaction Coverage
Cover all pairs of conditions in sort and basic blocks in eval
How did you specify your test suite ?
16
Specs for Working Programmers
1 void sort(int * a, int len) {
2
int i, t;
3
for (i=1; i<len; ++i) {
4
if (compare(a[i-1], a[i])) continue;
5
t=a[i];
6
a[i]=a[i-1];
7
a[i-1]=t;
8
}
9
return;
10 }
Constrained Inputs
Basic block coverage in sort
Each test case shall use list of 2 to 15 elements
How did you specify your test suite ?
17
Specs for Working Programmers
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Avoid Unfinished Code
Basic block coverage in example
Never call unimplemented
How did you specify your test suite ?
18
Simple Coverage Criteria ?
„Condition Coverage“
cover all program conditions
1 void foo( int x) {
2
int a = x > 2 && x < 5;
3
if (a) { 0; } else { 1; }
4 }
Commercial Tools
Coverage Meter, CTC++
BullseyeCoverage
Test suite
x =1; x = 4
Condition coverage ?
There is no general purpose formalism for white box
test case specification
!
100% coverage
83% coverage
Related Work
Coverage formalizations
Using Z (Vilkomir, Bowen FORTEST’08)
Temporal logics (Hong et al. TACAS’02)
Test case generation techniques
Random testing, fuzzing
Directed testing (Godefroid et al. PLDI’05)
Model-checking based (Beyer et al. ICSE’04)
BLAST query language (Beyer et al. SAS’04)
Challenge:
Systematic Approach to White Box Testing ?
Precise Semantics
Expressive Power
small number of orthogonal concepts suffice to express large classes of specifications
Simplicity and Code Independence
tool for the working programmer
simple specs easily expressible
relative stability during code refactoring
Database Analogy ?
Encapsulation of Language Specifics
easily adaptable to a large class of imperative programming languages
Tool Support for Real World Code
test case generation engines
Test Specification Language
Precise and simple formalism to describe test suites
Precise semantics
High expressive power
Simple specifications easily expressible
Suitable for working programmer
How did you specify your test suite ?
22
Algorithmic Solution
Tool for the working programmer
Applicability to real world C code (embedded systems)
Efficient test input generation engines
How did you specify your test suite ?
23
Query-Driven Program Testing
173
if (ctrl_io_in[SENS_IMPULS]) {
174
if (!lastImp){
if (ctrl_io_out[MOTOR_ON]) {
if (directionUp) {
177
++cnt;
178
} else {
179
--cnt;
180
}
181
}
182
else if (timImp>0) {
183
if (directionUp) {
184
++cnt;
185
} else {
186
--cnt;
187
}
188
}
189
}
190
}
191
if (ctrl_io_in[SENS_BOTTOM]) {
192
cnt = 0;
193
cntValid = TRUE;
194
}
195
lastImp = ctrl_io_in[SENS_IMPULS];
196
if (timImp>0) {
197
--timImp;
198
if (timImp==0) {
199
if (cmd!=CMD_NONE) {
200
cmd = CMD_NONE;
201
}
202
}
203
}
175
176
Source Code
Test Case
Generation
Engines
Test179,
Case
FQL193,
Spec
Lines
200
Test
Suite
Separation of Concerns
clean semantics
multiple engines
query dispatcher
stable query interface
Database
Relational
Database
Engine(s)
Result
Set
SQL Query
Vision:
SQL for Test Specifications
How did you specify your test suite ?
24
Query-Driven Program Testing
Source Code
Test Case
Generation
Engines
Test
Suite
FQL
Algorithmic approach: CAV’08, VMCAI’09
FQL Language Concept: ASE 2010
Existing engines:
• FShell: Based on CBMC (C Bounded Model Checker)
• FlleSh: Uses CPAchecker (Configurable Program Analysis)
http://code.forsyte.de/fshell
How did you specify your test suite ?
25
Applications of FQL/FShell
Source Code
Test Case
Generation
Engines
Test
Suite
FQL
•
•
•
•
•
Test case generation
Certification
Requirement-driven testing
Coverage Evaluation
Reasoning about test specifications
How did you specify your test suite ?
26
FQL Challenge:
Designing a Coverage Specification Language
Syntax of the program
Semantics of the program
Reasonably language independent
Easy to write
Easy to understand
Natural to use
Predictable performance
High expressive power
Tractable to evaluate
FQL Challenge:
Designing a Coverage Specification Language
Specification for basic block coverage
„for each basic block in the program
there is a test case in the test suite
which covers the basic block
1. Specifies a test suite, i.e., multiple test cases
2. Contains a universal quantifier
3. Assumes knowledge about programs.
What IS a basic block for a logic ?
4. Has a meaning independent of the program under test
Can be translated into concrete specifications for a fixed program
FQL Challenge:
Designing a Coverage Specification Language
Universal quantification ?
Programming language support ?
CFG view versus trace view ?
Language independence ?
Evolve path patterns / regular expressions into a more complex
formalism.
FQL Key Concept
Quoted Regular Expressions
A regular expression matches a word
A quoted regular expression matches a finite set of words
„a*“ + „ab|cd“
matches all sets {X,Y} where
- X matches „a*“
- Y matches „ab|cd“
{aaa, ab}, {a,cd}, {aaaaaaaaaaa,ab} etc.
Unquoted part without Kleene star finite sets
FQL Language Concept
Program Representation: Control Flow Automata
Single Test Case Specification
Test Suite Specification
How did you specify your test suite ?
31
Control Flow Automata (CFA)
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Henzinger et al. (POPL’02)
Edges
assume (conditional branches)
assignment
function call
function return
skip
Nodes: program locations
How did you specify your test suite ?
32
FQL Language Concept
Program Representation: Control Flow Automata
Single Test Case Specification
Test Suite Specification
How did you specify your test suite ?
33
Single Test Case Specification
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Cover line 4
cover “@4”
IN:a=2, d=0
Cover some statement
cover “ID”
IN: a=8192, d=0
How did you specify your test suite ?
34
Single Test Case Specification
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Cover line 4 or line 6
cover “@4+@6”
Cover a basic block
cover “@basicblockentry”
Here:
@basicblockentry tantamount to @4+@6+@7
How did you specify your test suite ?
35
Single Test Case Specification
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
ID*
Test case = execution (program path)
“cover line 4” means
execute some statement(s)
reach line 4
execute until program exit
ID*
cover “ID*[email protected]*”
IN:
a=2, d=0
How did you specify your test suite ?
36
Single Tests by Path Patterns
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
cover “ID* . @4 . ID* + ID* . @6 . ID*”
Path patterns are regular expressions
Kleene star (*)
Concatenation (.)
Alternative/Union (+)
(Could go beyond regular expressions …)
How did you specify your test suite ?
37
Specification by Path Patterns
Path Pattern Alphabet: Program Syntax and Semantics
o
Filter functions: interface to programming language syntax
o
Filter expressions
o
Assertions over program variables
o
CFA edges, nodes and paths
How did you specify your test suite ?
38
Alphabet: Filter Functions
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
cover “@conditionedge”
cover “@conditiongraph”
cover “@decisionedge”
cover “@call(unimplemented)”
cover “@func(example)”
Program independence
How did you specify your test suite ?
39
Alphabet: Filter Expressions
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
Graph operations on filters
cover “@7 | @decisionedge”
cover “not(@3)”
cover “setminus(@decisionedge,@6)”
cover “@decisionedge & @4”
How did you specify your test suite ?
40
Alphabet: Program Assertions
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
a==42
cover “{a==42}.@3”
IN: a=42, d=0
d!=0
cover “(@4+@6).{d!=0}”
IN: a=0, d=65536
How did you specify your test suite ?
41
FQL Language Concept
Program Representation: Control Flow Automata
Single Test Case Specifications
Test Suite Specifications
How did you specify your test suite ?
42
Coverage Patterns
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Cover if and else branch
?
Need more than one test case - a test suite
How did you specify your test suite ?
43
Coverage Patterns
Coverage patterns = quoted path patterns
Each generated path pattern must be covered
Path patterns may describe an infinite language
a* . b . a* + cd* = { b, c, ab, cd, aba,
cdd, aab, aaba, aabaa, ... }
But quoting operator blocks expansion:
“a* . b . a* + cd*” = { a*ba* + cd* }
“a* . b . a*” + “cd*” = { a*ba*, cd* }
Coverage patterns: Kleene star only within quotes
How did you specify your test suite ?
44
Coverage Patterns
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Cover if and else branch
cover “ID*[email protected]*” + “ID*[email protected]*”
2 words - 2 test goals
IN:
a=2, d=0
IN:
a=0, d=0
How did you specify your test suite ?
45
Coverage Patterns
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Can we cover pairs of lines?
“ID*”.(@4+@6+@7).”ID*”.(@4+@6+@7).”ID*”
Coverage pattern describes 9 test goals
IN:
a=67108864, d=0
IN:
a=0, d=0
How did you specify your test suite ?
46
Coverage Patterns
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Recall
@basicblockentry tantamount to @4+@6+@7
cover “ID*”.(@4+@6+@7).”ID*”.(@4+@6+@7).”ID*”
tantamount to
cover “ID*”.@basicblockentry.”ID*”.@basicblockentry.”ID*”
How did you specify your test suite ?
47
Specs with Edges, Nodes, Paths
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
cover @conditiongraph
= cover EDGES(@conditiongraph)
6 test goals, 3 test cases suffice:
a = 1, c = 1
a = 0, b = 0
a = 0, b = 1, c = 0
How did you specify your test suite ?
48
Specs with Edges, Nodes, Paths
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
cover NODES(@conditiongraph)
5 test goals, 2 test cases suffice:
a = 1, c = 1
a = 0, b = 0
How did you specify your test suite ?
49
Specs with Edges, Nodes, Paths
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
cover PATHS(@conditiongraph, 1)
1 = repetition bound to assure finiteness
5 test goals, 5 test cases required:
a = 1, c = 1
a = 0, b = 0
a = 0, b = 1, c = 0
a = 0, b = 1, c = 1
a = 1, c = 0
How did you specify your test suite ?
50
FQL Coverage Specifications
General form of coverage specification
in [scope]
Where ?
cover [test goals]
What ?
passing [constraints]
How ?
„For each test goal inside scope,
provide a test case which
matches the passing condition.“
“Restricted Scope of Analysis”
Condition coverage in function partition with test cases that reach
line 7 at least once.
in @FUNC(partition)
cover @CONDITIONEDGE
passing _*.@7._*
FQL Summary
Filter functions
@FILE(), @LINE(), @BASICBLOCKENTRY, @CONDITONEDGE,
@STMTYPE(), UNION, INTERSECT, SETMINUS, etc.
Encapsulate the interface to the programming language
CFA
view of program
Filter expressions
union, intersect, compose, not, id, setminus, etc.
Path Patterns
Regular expressions (or more) over filter functions, assertions,
{cond}, >=k, etc.
Coverage Patterns
Quoted regular expressions
Trace
view of program
Full Format FQL Queries
in scope cover goals passing constraints
scope: CFA transformer/filter function
goals: coverage pattern
constraints: path pattern
“For each test goal inside scope, provide a test case which
satisfies the passing constraints.”
in @func(partition) cover @conditionedge passing @7
Condition coverage in function partition with test cases that reach line 7 at
least once.
How did you specify your test suite ?
53
FQL Challenge:
Designing a Coverage Specification Language
Specification for basic block coverage
„for each basic block in the program
there is a test case in the test suite
which covers the basic block
1. Specifies a test suite, i.e., multiple test cases
2. Contains a universal quantifier
3. Assumes knowledge about programs.
What IS a basic block for a logic ?
4. Has a meaning independent of the program under test
Can be translated into set of path patterns for a fixed program
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Basic Block Coverage
Requires a test suite such that each basic block is executed at least
once
cover @basicblockentry
(at runtime)
cover @4+@6+@7
How did you specify your test suite ?
55
Standard Coverage Criteria
1 int partition(int a[], int left, int right) {
2
int v = a[right], i = left - 1, j = right, t;
3
for (;;) {
4
while (a[++i] < v) ;
5
while (j > left && a[--j] > v) ;
6
if (i >= j) break;
7
t = a[i]; a[i] = a[j]; a[j] = t;
8
}
9
t = a[i]; a[i] = a[right]; a[right] = t;
10 return i;
11 }
Basic Block Coverage
Requires a test suite such that each basic block is executed at least
once
cover @basicblockentry
How did you specify your test suite ?
56
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
Decision Coverage
Conditional statements evaluate to true/false
cover @decisionedge
How did you specify your test suite ?
57
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
Condition Coverage
Atomic conditions evaluate to true/false
cover @conditionedge
How did you specify your test suite ?
58
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
Condition/Decision Coverage
Union of condition and decision coverage
cover @conditionedge + @decisionedge
How did you specify your test suite ?
59
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
Multiple Condition Coverage
All Boolean combinations of atomic conditions in complex conditions
cover paths(@conditiongraph, 1)
How did you specify your test suite ?
60
Standard Coverage Criteria
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Def-Use Coverage
Cover all definition/use pairs of a variable d
cover @def(d).”not(@def(d))*”.@use(d)
How did you specify your test suite ?
61
New Coverage Criteria
1
2
3
4
5
6
7
8
9
10
11
12
13
void insert(int * a, int pos) {
...
}
int main(int argc, char * argv[]) {
int i;
int A[100];
for (i=0; i<100; ++i)
insert(A, i);
return 0;
}
Loop-Bounded Path Coverage
•
•
All paths through main and insert
Pass each statement two times
cover paths(@func(main) | @func(insert),2)
How did you specify your test suite ?
62
New Coverage Criteria
1 int partition(int a[], int left, int right) {
2
int v = a[right], i = left - 1, j = right, t;
3
for (;;) {
4
while (a[++i] < v) ;
5
while (j > left && a[--j] > v) ;
6
if (i >= j) break;
7
t = a[i]; a[i] = a[j]; a[j] = t;
8
}
9
t = a[i]; a[i] = a[right]; a[right] = t;
10 return i;
11 }
Cartesian Block Coverage
All pairs and triples of basic blocks in function partition
cover @basicblockentry->@basicblockentry+
@basicblockentry->@basicblockentry-> @basicblockentry
How did you specify your test suite ?
63
Specs for Working Programmers
1
2
3
4
5
6
7
8
int example(int a, int b, int c, int d)
{
if ((a || b) && c)
d = 0;
else
unimplemented();
return d*2;
}
Cover Specific Lines of Code
Lines 4 and 6
cover @4 + @6
How did you specify your test suite ?
64
Specs for Working Programmers
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
void eval(int * a, int first, int last) {
if (first > last) return;
printf("a[%d]=%d\n", first, a[first]);
eval(a+1, first+1, last);
return;
}
int main(int argc, char * argv[]) {
int i;
int A[100];
for (i=0; i<100; ++i)
insert(A, i);
eval(A, 0, 100);
return 0;
}
Restricted Scope of Analysis
Basic block coverage in function eval only
cover @basicblockentry & @func(eval)
How did you specify your test suite ?
65
Specs for Working Programmers
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
void sort(int * a, int len) {
int i, t;
for (i=1; i<len; ++i) {
if (compare(a[i-1], a[i])) continue;
t=a[i]; a[i]=a[i-1]; a[i-1]=t;
}
}
void eval(int * a, int len) {
int i;
for (i=0; i < 3; ++i)
printf("a[%d]=%d\n", i, a[i]);
}
int main(int argc, char * argv[]) {
int i; int A[100];
for (i=0; i < 100; ++i) sort(A, 100);
eval(A, 100);
return 0;
}
Interaction Coverage
Cover all pairs of conditions in sort and basic blocks in eval
cover (@conditionedge & @func(sort)) ->
(@basicblockentry & @func(eval))
How did you specify your test suite ?
66
Specs for Working Programmers
1 void sort(int * a, int len) {
2
int i, t;
3
for (i=1; i<len; ++i) {
4
if (compare(a[i-1], a[i])) continue;
5
t=a[i];
6
a[i]=a[i-1];
7
a[i-1]=t;
8
}
9
return;
10 }
Constrained Inputs
Basic block coverage in sort
Each test case shall use list of 2 to 15 elements
cover {len>=2} . {len<=15} . @basicblockentry & @func(sort)
How did you specify your test suite ?
67
Specs for Working Programmers
1
2
3
4
5
6
7
8
int example(int a, int d)
{
if (a)
d = 0;
else
unimplemented();
return d*2;
}
Avoid Unfinished Code
Basic block coverage in example
Never call unimplemented
cover @basicblockentry & @func(example)
passing ^not(@call(unimplemented))*$
How did you specify your test suite ?
68
Conclusions and Current Work
Source Code
Test Case
Generation
Engines
Test
Suite
FQL
Test specification language based on quoted regular expressions
Two test input generation engines
Current work
• Evaluation with partners from automotive and avionics industry
• Model-based testing / DO 178B
• Directed Software Verification
How did you specify your test suite ?
http://code.forsyte.de/fshell
69