Listing 1

[Invariant("Total>=0", Label = "The total items in a stack cannot be negative")]
public interface IStack
{
  int Total{get;}
  bool Empty{
    [Postcondition("Result <=> Total == 0", Label = "Emptiness of a stack")]
    get;
  }
  bool Full{get;}
  [Precondition("!Empty", Label = "Stack Underflow")]
  object Top {
    get;
    [Postcondition("Top == value", Label = "The Top changes")]
    set;
  }
  [Precondition("!Full", Label = "Stack Overflow")]
  [Postcondition("Top == x", Label = "Applying a LIFO policy")]
  [Postcondition("Total == Total.Old + 1", Label = "Increasing the stack size")]
  [Postcondition("!Empty", Label = "Non Emptiness")]
  void Push(object x);
  [Precondition("!Empty", Label = "Stack Underflow")]
  [Postcondition("Total == Total.Old - 1", Label = "Decreasing the stack size")]
  [Postcondition("!Full", Label = "Non Fullness")]
  void Pop();
  }
}

Listing 2

interface IAssertion{
  string BoolExpression {get;}
  string Label {get; set;}
  bool Inherited {get;}
}
abstract class AssertionAttribute:
System.Attribute, IAssertion {
  AssertionAttribute(string CSALExpression){
    boolExpression = CSALExpression;
  }
  public string BoolExpression{
    get {
      return boolExpression;
    }
  }
  public string Label{
    get {
      return label;
    }
    set {
      label = value;
    }
  }
  public Type ExceptionRaised
    get {
      return exceptionRaised;
    }
    set {
      exceptionRaised = value;
    }
  }
  public bool Inherited
  {
    get
    {
      return inherited ;
    }
    set
    {
      inherited = value ;
    }
  }
  bool inherited;
  string boolExpression;
  string label = """;
  Type exceptionRaised;
}
[AttributeUsage(
AttributeTargets.Class |
AttributeTargets.Struct |
AttributeTargets.Interface,
AllowMultiple = true)]
public class InvariantAttribute :
AssertionAttribute {
InvariantAttribute(string CSALExpression) :
base(CSALExpression){}
}
[AttributeUsage(
AttributeTargets.Method |
AttributeTargets.Property |
AttributeTargets.Constructor,
AllowMultiple = true)]
public class PreconditionAttribute :
AssertionAttribute {
PreconditionAttribute(string CSALExpression) :
base(CSALExpression){}
}
[AttributeUsage(
AttributeTargets.Method |
AttributeTargets.Property |
AttributeTargets.Constructor,
AllowMultiple = true)]
public class PostconditionAttribute :
AssertionAttribute {
PostconditionAttribute(string CSALExpression) :
base(CSALExpression){}
}

Listing 3

[Invariant(
@"(Year > 0) && (Day >= 1) && (Month >= 1) &&
(Month <= 12)
&&
(
((Month == 1) || (Month == 3) || (Month == 5)
|| (Month == 7) ||
(Month == 8) || (Month == 10) || (Month ==
12)
)
=> (Day <= 31)
||
((Month == 4) || (Month == 6) || (Month == 9) ||
(Month == 11)) => (Day <= 30)
||
((Month == 2) && (Year % 4 == 0)) => (Day <=
29)
||
((Month == 2) && (Year % 4 != 0)) => (Day <=
28)
)", Label = "Day and Month consistency of a
date")]
[Invariant("exists(Date d in Holidays : d ==
Christmas || d == NewYear)",Label = "Standard Western holidays")]

public class Date{
  public static ICollection Holidays {get;}
  [Postcondition("exists(Date d in Holidays : d == newHoliday)"]
  public static void AddHoliday(Date newHoliday);
  [Postcondition("forall(Date d in Holidays : d != wasHoliday)"]
  public static void RemoveHoliday(DatewasHoliday);
  public int Month {get; set;}
  public int Day {get; set;}
  public int Year {get; set;}
  [Precondition("d1 != null && d2 != null", Label = "Date parameters can not be null"]
  public static long operator - (Date d1, Date d2);
 
  public Date Tomorrow {
    [Postcondition("result - this == 1", Label = "Tomorrow is the day after today")]
    get;
  }
  //...Other Date resources
}