@@ -100,10 +100,43 @@ <h1><a name="Model-based-Testing-Experimental" class="anchor" href="#Model-based
100100 < span class ="k "> member</ span > < span onmouseout ="hideTip(event, 'fs10', 25) " onmouseover ="showTip(event, 'fs10', 25) " class ="id "> __</ span > < span class ="pn "> .</ span > < span class ="fn "> Reset</ span > < span class ="pn "> (</ span > < span class ="pn "> )</ span > < span class ="o "> =</ span > < span onmouseout ="hideTip(event, 'fs8', 26) " onmouseover ="showTip(event, 'fs8', 26) " class ="mv "> n</ span > < span class ="k "> <-</ span > < span class ="n "> 0</ span >
101101 < span class ="k "> override</ span > < span onmouseout ="hideTip(event, 'fs10', 27) " onmouseover ="showTip(event, 'fs10', 27) " class ="id "> __</ span > < span class ="pn "> .</ span > < span class ="fn "> ToString</ span > < span class ="pn "> (</ span > < span class ="pn "> )</ span > < span class ="o "> =</ span > < span onmouseout ="hideTip(event, 'fs12', 28) " onmouseover ="showTip(event, 'fs12', 28) " class ="fn "> sprintf</ span > < span class ="s "> "Counter = </ span > < span class ="pf "> %i</ span > < span class ="s "> "</ span > < span onmouseout ="hideTip(event, 'fs8', 29) " onmouseover ="showTip(event, 'fs8', 29) " class ="mv "> n</ span >
102102</ code > </ pre >
103- < p > As a model to test this class we can use an int value which is an abstraction of the object's internal state. The
104- idea is that each operation on the class (in this case, Inc, Dec and Reset) affects both the model object and the actual object, and
103+ < p > In C#:</ p >
104+ < table class ="pre "> < tr > < td class ="snippet "> < pre class ="fssnip highlighted "> < code lang ="csharp "> < span class ="k "> public</ span > < span class ="k "> class</ span > Counter
105+ {
106+ < span class ="k "> internal</ span > < span class ="k "> int</ span > N { get; < span class ="k "> private</ span > set; }
107+
108+ < span class ="k "> internal</ span > Counter(< span class ="k "> int</ span > n)
109+ {
110+ N < span class ="o "> =</ span > n;
111+ }
112+
113+ < span class ="k "> internal</ span > < span class ="k "> void</ span > Inc()
114+ {
115+ < span class ="k "> if</ span > (N < span class ="o "> <</ span > < span class ="o "> =</ span > < span class ="n "> 3</ span > )
116+ N < span class ="o "> +</ span > < span class ="o "> =</ span > < span class ="n "> 1</ span > ;
117+ < span class ="k "> else</ span >
118+ N < span class ="o "> =</ span > -N < span class ="o "> +</ span > < span class ="n "> 2</ span > ;
119+ }
120+
121+ < span class ="k "> internal</ span > < span class ="k "> void</ span > Dec()
122+ {
123+ < span class ="k "> if</ span > (N < span class ="o "> <</ span > < span class ="o "> =</ span > < span class ="n "> 0</ span > )
124+ < span class ="k "> throw</ span > < span class ="k "> new</ span > InvalidOperationException(< span class ="s "> "Precondition fail"</ span > );
125+
126+ N < span class ="o "> -</ span > < span class ="o "> =</ span > < span class ="n "> 1</ span > ;
127+ }
128+
129+ < span class ="k "> internal</ span > < span class ="k "> void</ span > Reset()
130+ {
131+ N < span class ="o "> =</ span > < span class ="n "> 0</ span > ;
132+ }
133+
134+ < span class ="k "> public</ span > < span class ="k "> override</ span > < span class ="k "> string</ span > ToString() < span class ="o "> =</ span > < span class ="o "> ></ span > $< span class ="s "> "Counter = {N}"</ span > ;
135+ }</ code > </ pre > </ td > </ tr > </ table >
136+ < p > As a model to test this class we can use an < code > int</ code > value which is an abstraction of the object's internal state. The
137+ idea is that each operation on the class (in this case, < code > Inc</ code > , < code > Dec</ code > and < code > Reset</ code > ) affects both the model object and the actual object, and
105138after each such operation, the model and the actual instance should still be equivalent.</ p >
106- < p > With this idea in mind, you can write a specification of the Counter class using an int model as follows:</ p >
139+ < p > With this idea in mind, you can write a specification of the < code > Counter</ code > class using an int model as follows:</ p >
107140< pre class ="fssnip highlighted "> < code lang ="fsharp "> < span class ="k "> let</ span > < span onmouseout ="hideTip(event, 'fs13', 30) " onmouseover ="showTip(event, 'fs13', 30) " class ="id "> spec</ span > < span class ="o "> =</ span >
108141 < span class ="k "> let</ span > < span onmouseout ="hideTip(event, 'fs14', 31) " onmouseover ="showTip(event, 'fs14', 31) " class ="fn "> inc</ span > < span class ="o "> =</ span >
109142 < span class ="pn "> {</ span > < span class ="k "> new</ span > < span onmouseout ="hideTip(event, 'fs15', 32) " onmouseover ="showTip(event, 'fs15', 32) " class ="rt "> Operation</ span > < span class ="pn "> <</ span > < span onmouseout ="hideTip(event, 'fs5', 33) " onmouseover ="showTip(event, 'fs5', 33) " class ="rt "> Counter</ span > < span class ="pn "> ,</ span > < span onmouseout ="hideTip(event, 'fs7', 34) " onmouseover ="showTip(event, 'fs7', 34) " class ="vt "> int</ span > < span class ="pn "> ></ span > < span class ="pn "> (</ span > < span class ="pn "> )</ span > < span class ="k "> with</ span >
@@ -131,6 +164,86 @@ <h1><a name="Model-based-Testing-Experimental" class="anchor" href="#Model-based
131164 < span class ="k "> member</ span > < span class ="id "> __</ span > < span class ="pn "> .</ span > < span class ="fn "> Setup</ span > < span class ="o "> =</ span > < span onmouseout ="hideTip(event, 'fs34', 92) " onmouseover ="showTip(event, 'fs34', 92) " class ="m "> Gen</ span > < span class ="pn "> .</ span > < span onmouseout ="hideTip(event, 'fs35', 93) " onmouseover ="showTip(event, 'fs35', 93) " class ="id "> choose</ span > < span class ="pn "> (</ span > < span class ="n "> 0</ span > < span class ="pn "> ,</ span > < span class ="n "> 3</ span > < span class ="pn "> )</ span > < span class ="o "> |></ span > < span onmouseout ="hideTip(event, 'fs34', 94) " onmouseover ="showTip(event, 'fs34', 94) " class ="m "> Gen</ span > < span class ="pn "> .</ span > < span onmouseout ="hideTip(event, 'fs36', 95) " onmouseover ="showTip(event, 'fs36', 95) " class ="id "> map</ span > < span onmouseout ="hideTip(event, 'fs28', 96) " onmouseover ="showTip(event, 'fs28', 96) " class ="fn "> create</ span > < span class ="o "> |></ span > < span onmouseout ="hideTip(event, 'fs37', 97) " onmouseover ="showTip(event, 'fs37', 97) " class ="m "> Arb</ span > < span class ="pn "> .</ span > < span onmouseout ="hideTip(event, 'fs38', 98) " onmouseover ="showTip(event, 'fs38', 98) " class ="id "> fromGen</ span >
132165 < span class ="k "> member</ span > < span onmouseout ="hideTip(event, 'fs39', 99) " onmouseover ="showTip(event, 'fs39', 99) " class ="id "> __</ span > < span class ="pn "> .</ span > < span onmouseout ="hideTip(event, 'fs40', 100) " onmouseover ="showTip(event, 'fs40', 100) " class ="fn "> Next</ span > < span class ="id "> _</ span > < span class ="o "> =</ span > < span onmouseout ="hideTip(event, 'fs34', 101) " onmouseover ="showTip(event, 'fs34', 101) " class ="m "> Gen</ span > < span class ="pn "> .</ span > < span onmouseout ="hideTip(event, 'fs41', 102) " onmouseover ="showTip(event, 'fs41', 102) " class ="id "> elements</ span > < span class ="pn "> [</ span > < span onmouseout ="hideTip(event, 'fs14', 103) " onmouseover ="showTip(event, 'fs14', 103) " class ="fn "> inc</ span > < span class ="pn "> ;</ span > < span onmouseout ="hideTip(event, 'fs25', 104) " onmouseover ="showTip(event, 'fs25', 104) " class ="fn "> dec</ span > < span class ="pn "> ]</ span > < span class ="pn "> }</ span >
133166</ code > </ pre >
167+ < p > In C#:</ p >
168+ < table class ="pre "> < tr > < td class ="snippet "> < pre class ="fssnip highlighted "> < code lang ="csharp "> < span class ="k "> private</ span > < span class ="k "> class</ span > CounterSpec
169+ {
170+ < span class ="k "> internal</ span > < span class ="k "> class</ span > Inc < span class ="o "> :</ span > Operation<Counter, < span class ="k "> int</ span > >
171+ {
172+ < span class ="k "> public</ span > < span class ="k "> override</ span > < span class ="k "> bool</ span > Pre(< span class ="k "> int</ span > m)
173+ {
174+ < span class ="k "> return</ span > m < span class ="o "> ></ span > < span class ="n "> 0</ span > ;
175+ }
176+
177+ < span class ="k "> public</ span > < span class ="k "> override</ span > < span class ="k "> int</ span > Run(< span class ="k "> int</ span > m)
178+ {
179+ < span class ="k "> return</ span > m < span class ="o "> +</ span > < span class ="n "> 1</ span > ;
180+ }
181+
182+ < span class ="k "> public</ span > < span class ="k "> override</ span > Property Check(Counter c, < span class ="k "> int</ span > m)
183+ {
184+ < span class ="k "> return</ span > (m < span class ="o "> =</ span > < span class ="o "> =</ span > c.N).Label($< span class ="s "> "Inc: model = {m}, actual = {c.N}"</ span > );
185+ }
186+
187+ < span class ="k "> public</ span > < span class ="k "> override</ span > < span class ="k "> string</ span > ToString() < span class ="o "> =</ span > < span class ="o "> ></ span > < span class ="s "> "inc"</ span > ;
188+ }
189+
190+ < span class ="k "> internal</ span > < span class ="k "> class</ span > Dec < span class ="o "> :</ span > Operation<Counter, < span class ="k "> int</ span > >
191+ {
192+ < span class ="k "> public</ span > < span class ="k "> override</ span > < span class ="k "> bool</ span > Pre(< span class ="k "> int</ span > m)
193+ {
194+ < span class ="k "> return</ span > m < span class ="o "> ></ span > < span class ="n "> 0</ span > ;
195+ }
196+
197+ < span class ="k "> public</ span > < span class ="k "> override</ span > < span class ="k "> int</ span > Run(< span class ="k "> int</ span > m)
198+ {
199+ < span class ="k "> return</ span > m < span class ="o "> -</ span > < span class ="n "> 1</ span > ;
200+ }
201+
202+
203+ < span class ="k "> public</ span > < span class ="k "> override</ span > Property Check(Counter c, < span class ="k "> int</ span > m)
204+ {
205+ c.Dec();
206+ < span class ="k "> return</ span > (m < span class ="o "> =</ span > < span class ="o "> =</ span > c.N).Label($< span class ="s "> "Dec: model = {m}, actual = {c.N}"</ span > );
207+ }
208+
209+ < span class ="k "> public</ span > < span class ="k "> override</ span > < span class ="k "> string</ span > ToString() < span class ="o "> =</ span > < span class ="o "> ></ span > < span class ="s "> "dec"</ span > ;
210+ }
211+
212+ < span class ="k "> internal</ span > < span class ="k "> class</ span > CounterSetup < span class ="o "> :</ span > Setup<Counter, < span class ="k "> int</ span > >
213+ {
214+ < span class ="k "> private</ span > < span class ="k "> readonly</ span > < span class ="k "> int</ span > _initialValue;
215+
216+ < span class ="k "> internal</ span > CounterSetup(< span class ="k "> int</ span > initialValue)
217+ {
218+ _initialValue < span class ="o "> =</ span > initialValue;
219+ }
220+
221+ < span class ="k "> public</ span > < span class ="k "> override</ span > Counter Actual() < span class ="o "> =</ span > < span class ="o "> ></ span > < span class ="k "> new</ span > (_initialValue);
222+
223+ < span class ="k "> public</ span > < span class ="k "> override</ span > < span class ="k "> int</ span > Model() < span class ="o "> =</ span > < span class ="o "> ></ span > _initialValue;
224+ }
225+ }
226+
227+ < span class ="k "> public</ span > < span class ="k "> class</ span > Specification < span class ="o "> :</ span > Machine<Counter, < span class ="k "> int</ span > >
228+ {
229+ < span class ="k "> public</ span > Specification(< span class ="k "> int</ span > maxNumberOfCommands) < span class ="o "> :</ span > < span class ="k "> base</ span > (maxNumberOfCommands) { }
230+
231+ < span class ="k "> public</ span > < span class ="k "> override</ span > Arbitrary<Setup<Counter, < span class ="k "> int</ span > >< span class ="o "> ></ span > Setup < span class ="o "> =</ span > < span class ="o "> ></ span >
232+ Arb.From(Gen.Choose(< span class ="n "> 0</ span > , < span class ="n "> 3</ span > )
233+ .Select<< span class ="k "> int</ span > , Setup<Counter, < span class ="k "> int</ span > >< span class ="o "> ></ span > (i < span class ="o "> =</ span > < span class ="o "> ></ span > < span class ="k "> new</ span > CounterSpec.CounterSetup(i)));
234+
235+ < span class ="k "> public</ span > < span class ="k "> override</ span > TearDown<Counter> TearDown < span class ="o "> =</ span > < span class ="o "> ></ span > < span class ="k "> new</ span > DisposeCall<Counter>();
236+
237+ < span class ="k "> public</ span > < span class ="k "> override</ span > Gen<Operation<Counter, < span class ="k "> int</ span > >< span class ="o "> ></ span > Next(< span class ="k "> int</ span > _) < span class ="o "> =</ span > < span class ="o "> ></ span >
238+ Gen.Elements(< span class ="k "> new</ span > Operation<Counter, < span class ="k "> int</ span > >[]
239+ {
240+ < span class ="k "> new</ span > CounterSpec.Inc(),
241+ < span class ="k "> new</ span > CounterSpec.Dec()
242+ });
243+
244+ < span class ="k "> public</ span > < span class ="k "> override</ span > IEnumerable<FSharpList<Operation<Counter, < span class ="k "> int</ span > >< span class ="o "> ></ span > < span class ="o "> ></ span > ShrinkOperations(FSharpList<Operation<Counter, < span class ="k "> int</ span > >< span class ="o "> ></ span > operation) < span class ="o "> =</ span > < span class ="o "> ></ span >
245+ < span class ="k "> base</ span > .ShrinkOperations(operation);
246+ }</ code > </ pre > </ td > </ tr > </ table >
134247< p > Let's break this down a bit. A specification is put together as an object that is a subtype of the abstract class < code > Machine<'TypeUnderTest,'ModelType></ code > .
135248What you're actually defining is a state machine which can simultaneously apply operations, or state transitions, to the actual system
136249under test (in this case, a simple object) and a model of the system under test.</ p >
@@ -152,22 +265,20 @@ <h1><a name="Model-based-Testing-Experimental" class="anchor" href="#Model-based
152265calls < code > Inc()</ code > or < code > Dec()</ code > on the < code > Counter</ code > instance, and checks that after that the model counter is equal to the real < code > Counter</ code > . < code > Dec</ code > in addition has a (quite
153266silly, for demonstration purposes) precondition that the value should be strictly greater than 0 - if we run this machine our < code > Counter</ code > throws if we call < code > Dec</ code >
154267so when we run this specification we can check that FsCheck does the right thing here (testing the test library, very meta...)</ p >
155- < p > We also override ToString in each < code > Operation</ code > so that counter-examples can be printed.</ p >
268+ < p > We also override < code > ToString</ code > in each < code > Operation</ code > so that counter-examples can be printed.</ p >
156269< p > A specification can be checked as follows:</ p >
157270< pre class ="fssnip highlighted "> < code lang ="fsharp "> < span onmouseout ="hideTip(event, 'fs42', 105) " onmouseover ="showTip(event, 'fs42', 105) " class ="rt "> Check</ span > < span class ="pn "> .</ span > < span onmouseout ="hideTip(event, 'fs43', 106) " onmouseover ="showTip(event, 'fs43', 106) " class ="id "> Quick</ span > < span class ="pn "> (</ span > < span onmouseout ="hideTip(event, 'fs44', 107) " onmouseover ="showTip(event, 'fs44', 107) " class ="m "> StateMachine</ span > < span class ="pn "> .</ span > < span onmouseout ="hideTip(event, 'fs45', 108) " onmouseover ="showTip(event, 'fs45', 108) " class ="id "> toProperty</ span > < span onmouseout ="hideTip(event, 'fs13', 109) " onmouseover ="showTip(event, 'fs13', 109) " class ="id "> spec</ span > < span class ="pn "> )</ span >
158271</ code > </ pre >
159- < table class ="pre "> < tr > < td > < pre > < code > Falsifiable, after 6 tests (4 shrinks) (12770152580777276754,10005441753482479477 )
160- Last step was invoked with size of 7 and seed of (17861426896115535097,11667813865249411481 ):
272+ < table class ="pre "> < tr > < td > < pre > < code > Falsifiable, after 4 tests (2 shrinks) (14366654795077628011,16084604498746219839 )
273+ Last step was invoked with size of 5 and seed of (16085007916889491838,9608441260416857165 ):
161274Label of failing property: Inc: model = 5, actual = 6
162275Original:
163276(2, Setup Counter)
164- dec -> 1
165- inc -> 2
166277inc -> 3
167278inc -> 4
168279inc -> 5
169280dec -> 4
170- dec -> 3
281+ inc -> 5
171282
172283Shrunk:
173284(2, Setup Counter)
0 commit comments