Sample C# code for Model-base testing (#702)

* C# code for Counter

* Type and method names are formatted as code

* C# code for model-base test specification

Author: arialdomartini

docs/StatefulTestingNew.fsx

@@ -25,12 +25,15 @@ type Counter(?initial:int) =
     member __.Reset() = n <- 0
     override __.ToString() = sprintf "Counter = %i" n
 
-(**
-As a model to test this class we can use an int value which is an abstraction of the object's internal state. The
-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 
+(** In C#:
+
+    [lang=csharp,file=../examples/CSharp.DocSnippets/StatefulTesting.cs,key=Counter]
+
+As a model to test this class we can use an `int` value which is an abstraction of the object's internal state. The
+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 
 after each such operation, the model and the actual instance should still be equivalent.
 
-With this idea in mind, you can write a specification of the Counter class using an int model as follows:*)
+With this idea in mind, you can write a specification of the `Counter` class using an int model as follows:*)
 
 let spec =
     let inc = 
@@ -60,6 +63,12 @@ let spec =
         member __.Next _ = Gen.elements [ inc; dec ] }
 
 (**
+
+ In C#:
+
+    [lang=csharp,file=../examples/CSharp.DocSnippets/StatefulTesting.cs,key=Specification]
+
+
 Let's break this down a bit. A specification is put together as an object that is a subtype of the abstract class `Machine<'TypeUnderTest,'ModelType>`. 
 What you're actually defining is a state machine which can simultaneously apply operations, or state transitions, to the actual system
 under test (in this case, a simple object) and a model of the system under test.
@@ -88,7 +97,7 @@ calls `Inc()` or `Dec()` on the `Counter` instance, and checks that after that t
 silly, for demonstration purposes) precondition that the value should be strictly greater than 0 - if we run this machine our `Counter` throws if we call `Dec` 
 so when we run this specification we can check that FsCheck does the right thing here (testing the test library, very meta...)
 
-We also override ToString in each `Operation` so that counter-examples can be printed.
+We also override `ToString` in each `Operation` so that counter-examples can be printed.
 
 A specification can be checked as follows:*)
 

examples/CSharp.DocSnippets/StatefulTesting.cs

@@ -0,0 +1,138 @@
+namespace CSharp.DocSnippets;
+
+using System;
+using System.Collections.Generic;
+using FsCheck;
+using FsCheck.Experimental;
+using FsCheck.Fluent;
+using Microsoft.FSharp.Collections;
+using Xunit;
+
+public class StatefulTesting
+{
+    //[Counter]
+    public class Counter
+    {
+        internal int N { get; private set; }
+
+        internal Counter(int n)
+        {
+            N = n;
+        }
+
+        internal void Inc()
+        {
+            if (N <= 3)
+                N += 1;
+            else
+                N = -N + 2;
+        }
+
+        internal void Dec()
+        {
+            if (N <= 0)
+                throw new InvalidOperationException("Precondition fail");
+
+            N -= 1;
+        }
+
+        internal void Reset()
+        {
+            N = 0;
+        }
+
+        public override string ToString() => $"Counter = {N}";
+    }
+    //[/Counter]
+
+    //[Specification]
+    private class CounterSpec
+    {
+        internal class Inc : Operation<Counter, int>
+        {
+            public override bool Pre(int m)
+            {
+                return m > 0;
+            }
+
+            public override int Run(int m)
+            {
+                return m + 1;
+            }
+
+            public override Property Check(Counter c, int m)
+            {
+                return (m == c.N).Label($"Inc: model = {m}, actual = {c.N}");
+            }
+
+            public override string ToString() => "inc";
+        }
+
+        internal class Dec : Operation<Counter, int>
+        {
+            public override bool Pre(int m)
+            {
+                return m > 0;
+            }
+
+            public override int Run(int m)
+            {
+                return m - 1;
+            }
+
+
+            public override Property Check(Counter c, int m)
+            {
+                c.Dec();
+                return (m == c.N).Label($"Dec: model = {m}, actual = {c.N}");
+            }
+
+            public override string ToString() => "dec";
+        }
+
+        internal class CounterSetup : Setup<Counter, int>
+        {
+            private readonly int _initialValue;
+
+            internal CounterSetup(int initialValue)
+            {
+                _initialValue = initialValue;
+            }
+
+            public override Counter Actual() => new(_initialValue);
+
+            public override int Model() => _initialValue;
+        }
+    }
+
+    public class Specification : Machine<Counter, int>
+    {
+        public Specification(int maxNumberOfCommands) : base(maxNumberOfCommands) { }
+
+        public override Arbitrary<Setup<Counter, int>> Setup =>
+            Arb.From(Gen.Choose(0, 3)
+                .Select<int, Setup<Counter, int>>(i => new CounterSpec.CounterSetup(i)));
+
+        public override TearDown<Counter> TearDown => new DisposeCall<Counter>();
+        
+        public override Gen<Operation<Counter, int>> Next(int _) =>
+            Gen.Elements(new Operation<Counter, int>[]
+            {
+                new CounterSpec.Inc(), 
+                new CounterSpec.Dec()
+            });
+
+        public override IEnumerable<FSharpList<Operation<Counter, int>>> ShrinkOperations(FSharpList<Operation<Counter, int>> operation) => 
+            base.ShrinkOperations(operation);
+    }
+    //[/Specification]
+
+    
+    [Fact]
+    void counter_tested_with_stateful_testing()
+    {
+        var property = new Specification(10).ToProperty();
+
+        Check.QuickThrowOnFailure(property);
+    }
+}