// ------------------------------------------------------------------

// Post.cs: Represents OCL testing for Postconditions

// ------------------------------------------------------------------

// Project: C# and OCL Compiler

// Module:  Testing

// Author:  Dave Arnold

// Version: 1.0

// ------------------------------------------------------------------

 

// ------------------------------------------------------------------

// Imports

// ------------------------------------------------------------------

using System;

using System.Collections;

// ------------------------------------------------------------------

 

// ------------------------------------------------------------------

// DaveArnold.OCLTesting Namespace

// ------------------------------------------------------------------

namespace DaveArnold.OCLTesting

{

       // A Class to test Postconditions

       class PostTests

       {

              OCL

              [

                     "context PostTests::Square(a : Integer): Integer"

                     "pre: a > 0"

              ]

             

              OCL

              [

                     "context PostTests::Square(a : Integer): Integer"

                     "pre: a > 5"

              ]

             

              OCL

              [

                     "context PostTests::Square(a : Integer): Integer"

                     "post: a > 2"

              ]

             

              OCL

              [

                     "context PostTests::Square(a : Integer): Integer"

                     "post: result = a * a"

              ]

             

              public int Square(int a)

              { return a*a;}

             

              private int age = 24;

             

              OCL

              [

                     "context PostTests::SQAge get : Integer"

                     "post: result = age * age"

              ]

              public int SQAge

              {

             

                     get { return age * age; }

              }

             

              OCL

              [

                     "context PostTests::Age set : Integer"

                     "pre: value > 24"

                     "post: age = value"

              ]

              public int Age

              {

                     set { age = value; }

              }

             

              OCL

              [

                     "context PostTests::Birthday(): OclVoid"

                     "post: age = age@pre + 1"

              ]

              public void Birthday()

              {

               age++;

              }

             

              OCL

              [

                     "context PostTests indexer(i : Integer) get: Integer"

                     "post: result = i * i"

              ]

              public int this[int i]

              {

                     get { return i * i; }

              }

             

              public void RunTests()

              {

                     Console.WriteLine("---------------- POST TESTS -----------------");

                     Console.WriteLine("P1 (Square(6)): {0}", Square(6));

                     Console.WriteLine("P2 (Birthday())");

                     Birthday();

                     Console.WriteLine("P3 (SQAge): {0}", SQAge);

                     Console.WriteLine("P4 (Age = 25)");

                     Age = 25;

                     Console.WriteLine("P5 (this[2]): {0}", this[2]);

                     Console.WriteLine("------------ POST TESTS COMPLETE ------------");

              }

       }

}

 

// ------------------------------------------------------------------

// EOF