1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
|
/*-------------------------------------------------------------------------*\
** ScalaCheck **
** Copyright (c) 2007-2010 Rickard Nilsson. All rights reserved. **
** http://www.scalacheck.org **
** **
** This software is released under the terms of the Revised BSD License. **
** There is NO WARRANTY. See the file LICENSE for the full text. **
\*-------------------------------------------------------------------------*/
package org.scalacheck
import Gen._
import Prop._
import Shrink._
/** See User Guide for usage examples */
trait Commands extends Prop {
/** The abstract state data type. This type must be immutable.
* The state type that encodes the abstract state. The abstract state
* should model all the features we need from the real state, the system
* under test. We should leave out all details that aren't needed for
* specifying our pre- and postconditions. The state type must be called
* State and be immutable. */
type State <: AnyRef
class Binding(private val key: State) {
def get: Any = bindings.find(_._1 eq key) match {
case None => sys.error("No value bound")
case Some(x) => x
}
}
/** Abstract commands are defined as subtypes of the traits Command or SetCommand.
* Each command must have a run method and a method that returns the new abstract
* state, as it should look after the command has been run.
* A command can also define a precondition that states how the current
* abstract state must look if the command should be allowed to run.
* Finally, we can also define a postcondition which verifies that the
* system under test is in a correct state after the command exectution. */
trait Command {
/** Used internally. */
protected[Commands] def run_(s: State) = run(s)
def run(s: State): Any
def nextState(s: State): State
/** @deprecated Use <code>preConditions += ...</code> instead. */
@deprecated("Use 'preConditions += ...' instead.")
def preCondition_=(f: State => Boolean) = {
preConditions.clear
preConditions += f
}
/** Returns all preconditions merged into a single function */
def preCondition: (State => Boolean) = s => preConditions.toList.forall(_.apply(s))
/** A precondition is a function that
* takes the current abstract state as parameter and returns a boolean
* that says if the precondition is fulfilled or not. You can add several
* conditions to the precondition list */
val preConditions = new collection.mutable.ListBuffer[State => Boolean]
/** @deprecated Use <code>postConditions += ...</code> instead. */
@deprecated("Use 'postConditions += ...' instead.")
def postCondition_=(f: (State,Any) => Prop) = {
postConditions.clear
postConditions += ((s0,s1,r) => f(s0,r))
}
/** @deprecated Use <code>postConditions += ...</code> instead. */
@deprecated("Use 'postConditions += ...' instead.")
def postCondition_=(f: (State,State,Any) => Prop) = {
postConditions.clear
postConditions += f
}
/** Returns all postconditions merged into a single function */
def postCondition: (State,State,Any) => Prop = (s0,s1,r) => all(postConditions.map(_.apply(s0,s1,r)): _*)
/** A postcondition is a function that
* takes three parameters, s0, s1 and r. s0 is the abstract state before
* the command was run, s1 is the abstract state after the command was
* run, and r is the result from the command's run
* method. The postcondition function should return a Boolean (or
* a Prop instance) that says if the condition holds or not. You can add several
* conditions to the postConditions list. */
val postConditions = new collection.mutable.ListBuffer[(State,State,Any) => Prop]
}
/** A command that binds its result for later use */
trait SetCommand extends Command {
/** Used internally. */
protected[Commands] final override def run_(s: State) = {
val r = run(s)
bindings += ((s,r))
r
}
final def nextState(s: State) = nextState(s, new Binding(s))
def nextState(s: State, b: Binding): State
}
private case class Cmds(cs: List[Command], ss: List[State]) {
override def toString = cs.map(_.toString).mkString(", ")
}
private val bindings = new scala.collection.mutable.ListBuffer[(State,Any)]
private def initState() = {
bindings.clear()
initialState()
}
private def genCmds: Gen[Cmds] = {
def sizedCmds(s: State)(sz: Int): Gen[Cmds] =
if(sz <= 0) value(Cmds(Nil, Nil)) else for {
c <- genCommand(s) suchThat (_.preCondition(s))
Cmds(cs,ss) <- sizedCmds(c.nextState(s))(sz-1)
} yield Cmds(c::cs, s::ss)
for {
s0 <- wrap(value(initialState()))
cmds <- sized(sizedCmds(s0))
} yield cmds
}
private def validCmds(s: State, cs: List[Command]): Option[Cmds] =
cs match {
case Nil => Some(Cmds(Nil, s::Nil))
case c::_ if !c.preCondition(s) => None
case c::cmds => for {
Cmds(_, ss) <- validCmds(c.nextState(s), cmds)
} yield Cmds(cs, s::ss)
}
private def runCommands(cmds: Cmds): Prop = cmds match {
case Cmds(Nil, _) => proved
case Cmds(c::cs, s::ss) =>
c.postCondition(s,c.nextState(s),c.run(s)) && runCommands(Cmds(cs,ss))
case _ => sys.error("Should not be here")
}
private def commandsProp: Prop = {
def shrinkCmds(cmds: Cmds) = cmds match { case Cmds(cs,_) =>
shrink(cs)(shrinkContainer).flatMap(cs => validCmds(initialState(), cs).toList)
}
forAllShrink(genCmds label "COMMANDS", shrinkCmds)(runCommands _)
}
def apply(p: Prop.Params) = commandsProp(p)
/** initialState should reset the system under test to a well defined
* initial state, and return the abstract version of that state. */
def initialState(): State
/** The command generator. Given an abstract state, the generator
* should return a command that is allowed to run in that state. Note that
* it is still neccessary to define preconditions on the commands if there
* are any. The generator is just giving a hint of which commands that are
* suitable for a given state, the preconditions will still be checked before
* a command runs. Sometimes you maybe want to adjust the distribution of
* your command generator according to the state, or do other calculations
* based on the state. */
def genCommand(s: State): Gen[Command]
}
|