.NET assemblies are superior to previous component
technologies because they seamlessly provide multilingual support;
introduce an excellent synergy between code and metadata; and inspire
confidence through a strong type system and the .NET security policy.
Nevertheless, .NET lacks a formal mechanism for specifying the
semantics of the types offered by an assembly.
This article shows how, using .NET attributes, it is feasible
to introduce Boolean assertion clauses in .NET assemblies. Using
reflection, these assertion attributes can be extracted, checked, and
monitored at runtime. We offer an assertion browser tool that
extracts the assertion attributes from the assemblies for
documentation purposes and generates a "trusted" proxy assembly to
monitor these assertions at runtime.
.NET introduces a new metadata feature: attributes. Through
attributes we can include our own custom metadata in assemblies.
The Convenience of More Trusted .NET Assemblies
The .NET signing policy is based on confidence in the human
(enterprise) author of the assembly, but this is not enough for
reliability. Applications are not forced to use the types of an
assembly under the "contract" that these types request (in the BCL
these "contracts" appear in a verbose fashion). We need a more
organized documentation to verify that an assembly does what it says
it does.
How can an assembly exporting a type Stack, with a Push
method and a property Top, prohibit its client assemblies from
applying Top to a stack s if s is empty? How can the same assembly
guarantee that after pushing an object x in s, the property Top will
return x?
Including Assertions by Means of .NET Attributes
The proposed assertions are represented by the interface:
interface IAssertion{
string BoolExpression {get;}
string Label {get; set;}
bool Inherited {get;}
}
The class AssertionAttribute implements IAssertion and
extends the .NET SystemAttribute. This class allows the inclusion of
the assertion attributes in the source code during compilation.
The target of an assertion attribute will be a type or a method (including properties and
constructors). The assembly resulting from the compilation of a
project with those assertion attributes will be called the asserted assembly.
The assertions are really the raw string parameters of these attri-
butes, which are returned by the property BoolExpression. They must
denote logical expressions under a notation named C#AL (C#-like
Assertion Language).
For example, the string "!Empty" used in the assertion
attribute of the method Pop (see Listing 1) helps to specify that a
stack cannot be popped if it is empty.
The property Label = "To pop an element the stack cannot be
empty" defines a textual message about the assertion's semantics.
The Inherited property states whether the assertion will also
apply to a derived type or method.
The AssertionAttribute class has three derived types. The Invariant-
Attribute derives from Assertion-Attribute. The AttributeUsage attribute is used to define the possible targets of this
InvariantAttribute, which in this case are classes, interfaces, or
structs (see Listing 2).
For an InvariantAttribute the BoolExpression should be true
before and after applying any public method of the type attached to
the attribute.
Because the property Allow-Multiple is set to true, several invariant attributes can be targeted
to a single type. A logical conjunction (&&) will be applied to all
Boolean expressions.
When assertions are monitored during runtime and && evaluates
to false, then an InvariantException will be thrown. The Label
property will be part of the exception message.
The following excerpt shows an invariant attribute attached
to a Rational type:
[Invariant("Denominator != 0", Label="Denominator cannot be zero")]
struct Rational{
...
public int Numerator{
...
}
public int Denominator{
...
}
}
PreconditionAttribute and PostconditionAttribute also derive
from AssertionAttribute. Under the Design by Contract guidelines, a
PreconditionAttribute denotes a condition required by the assembly
before applying the public method targeted by the attribute, and a
PostconditionAttribute denotes a condition that will be ensured by
the assembly after applying the method targeted by the attribute.
Note: The Push method of the Stack type (see Listing 1) has
three postconditions (the property AllowMultiple of the Post-
conditionAttribute is true).
interface Stack {
...
[Precondition("!Full",
Label="Stack Overflow")]
[Postcondition("!Empty")]
[Postcondition("Total == Total.Old + 1")]
[Postcondition("Top == x", Label="The Stack applies a
LIFO policy")]
public void Push(object x);
...
}
The attribute [Precondition
("!Full", Label="Stack Overflow")] states that to push the stack, it
cannot be full; the attribute [Postcondition("!Empty")] states that
after pushing, the stack will not be empty; and the [Postcondition
("Total == Total.Old + 1")] states that the total of elements in the
stack will be one plus the old value of Total before executing the
push. The attribute [Postcondition("Top == x", Label="The Stack
applies a LIFO policy")] means that the pushed element will be at the
top of the stack.
The InvariantException, PreconditionException, and
PostconditionException types, derived from the base class
AssertionException, represent the exceptions to be thrown when the
corresponding assertion is not fulfilled at runtime.
Assertion Attributes and Inheritance
An invariant defined in a base type must be fulfilled by the
instances of each derived type. Preconditions and postconditions
targeting a virtual base method must be fulfilled by the
corresponding overriding method.
The above approach fits well with classes implementing an
interface base type, but it should not necessarily be applied when a
class extends another base class. If the Inheritable property is set
to false, a developer of a derived method is not forced to guarantee
the assertions of the corresponding base method. For example, the
following class Account does not require a derived class
CreditAccount to conform to the precondition "Balance > amount" when
overriding the method Withdraw, because a CreditAccount allows a
negative Balance.
class Account{
..
[Precondition("Balance >
amount")]
[Postcondition("Balance ==
Balance.Old - amount")]
public virtual void Withdraw(intamount){
...
}
}
The C# Assertion Language (C#AL)
Each BoolExpression parameter in the assertion attributes
must describe a C#-like Boolean expression (an analogous approach
could be applied to other .NET languages). An entity appearing in the
expression must observe the following rules:
1. It must be public in order to be used and tested by client
code in other assemblies. If the Full property of the Stack type (see
Listing 1) were not public, then it would make no sense for the
method Push to have the precondition "!Full".
2. Pre- and postconditions of an instance method can use both
instance and static features of the type defining the method.
3. Pre- and postconditions of a static method can use only the
type's static features.
C#AL includes a special property, Old, which can be applied
to any term used in a method's postcondition. This property returns
the corresponding value of the term before the method's execution.
The attribute
[Postcondition("Total == Total.Old + 1",Label="The stack must
increase by one element"]
attached to the Push method, expresses that after pushing an element,
the Total property must return a value equal to the value of Total
before the execution of Push (denoted by Total.Old) increased by 1.
When x is of reference type x.Old returns a copy of the
reference. But if the dynamic type of the object attached to x
implements the interface ICloneable, the returned value is a clone of
x. So by implementing the method Clone and overriding the method
Equals, developers can decide how deeply to apply the Old policy.
A special variable, "result," can be used in the
postcondition of a nonvoid method; it will refer to the returning
value of the method. For example, the property Tomorrow (see Listing
3) has the postcondition:
[Postcondition("result-this == 1",
Label = "Tomorrow is the day after today")]
Others operators are => (implies) and <=> (if only if). These
operators facilitate design and improve readability, as shown in the
invariant assertion attribute of the Date type (see Listing 3).
Quantifiers in C#AL
Several previous papers have recognized the relevance of
quantifiers in assertions. Fortunately .NET standardizes the notion
of collection based on the IEnumerable interface. Furthermore, C# includes the foreach operator. So,
based on these features, C#AL includes the universal quantifier
"forall" and the existential quantifier "exists":
forall (T x in C : E)
and
exists (T x in C : E)
where T is a type, x is a variable, C is an expression denoting a
collection of returning objects of some type that can be cast to T,
and E is a Boolean expression in which the variable x should appear.
The forall operator evaluates true if for all x in C the
expression E evaluates to true; otherwise it evaluates to false. The
operator exists evaluates to true if at least one x in C exists such
that the expression E evaluates to true; otherwise it evaluates to
false.
Both operators will throw an InvalidCast exception if the
object returned by the iteration cannot be cast to T. If you want to
apply an assertion to only a subset of C, you can use the following
pattern:
forall (object x in C : (x is T) => E')
where E' is the expression resulting from changing all occurrences of
x in E by the cast (T)x.
An Employee type having a property MyDepartment and a
Department type having an Employees property could have the following
invariants:
[Invariant("forall (Employee e in Employees : e.MyDepartment ==
this)",Label = "Legal Department")]
class Department {
...
}
[Invariant("exists (Employee e in MyDepartment.Employees : e ==
this)",Label = "Legal employee")]
class Employee {
...
}
Quantifiers are also helpful in postconditions and
preconditions. For example, a Fire method of the Department type
might have the postcondition:
[Postcondition("! exists (e in Employees: x == e)"]
public void Fire(Employee e){...}
A method, AnnounceMeeting, announces a meeting date but
requires that the date will not be a holiday:
[Precondition("forall (Date d in Date.Holidays : d != meetingDate")]
public void AnnounceMeeting(Date meetingDate){...}
The forthcoming iterator construct announced for C# will
offer better support for these C#AL quantifiers.
About Implementation
The assembly Assertion
Engine.dll contains all attribute types presented in the previous sections.
An application can use an asserted assembly as any ordinary
.NET assembly, ignoring the assertion attributes embedded in it.
Nevertheless, an application can also retrieve and study these
assertions for documentation purposes and can also evaluate them to
monitor the behavior of the features targeted by the assertion
attributes. For these purposes the AssertionEngine.dll includes the
AssertionManager type. Using reflection, AssertionManager retrieves
Assertion objects from the asserted assembly at runtime (the
Assertion class implements IAssertion).
But developers don't need to use the above capabilities
programmatically. A browser tool (see Figure 1) allows selection of
an assembly, and listing of the types, methods, and assertions in the
assembly.
The Documentation Panel generates an HTML file (Figure 2
illustrates the displayed HTML for the Stack type).
The following is a typical scenario: you are developing an
application using an asserted A.dll. You can use the C#AL browser to
visualize the assertion attributes embedded in A.dll and check if
they are correct. If you want to monitor the assertions, then you can
use the "Build" button (see Figure 1) to generate a trusted assembly,
Trusted_A.dll, which works as a proxy to the original A, intercepting
calls to the asserted A methods and evaluating the code of the
corresponding assertions. Finally, you must rebuild your project,
removing the reference to A.dll and including references to the new
Trusted_A.dll and to the AssertionEngine.dll. The resulting .exe file
will monitor the assertion's fulfillment.
Conclusion and Further Work
Unfortunately the .NET Framework did not include an assertion
mechanism from the outset. There is an Assert method in the Debug
class, but it is not enough to achieve the specification goal of
assertions.The Monash group is considering support assertions in the
Rotor runtime.
eXtensible C# (www.resolvecorp.com) includes declarative assertions. At present this approach is less expressive than C#AL.
Moreover, the C#AL browser tool allows you to insert
assertions in existing assemblies. We are also working on an
implementation of assertions using CodeDom. In this case the
Trusted_A.dll will not act as a proxy, but will embed its own A code.
Assertions are not enough to completely guarantee a
component's quality and behavior, according to Beugnard et al. in
their article, "Making Components Contract Aware" [Computer, Vol. 32,
No. 7]. Nevertheless, we hope that the proposed inclusion of
assertion attributes in .NET will be a humble but important step
toward the goal of a trusted component scenario.
This article illustrates the significance of .NET attributes
for metaprogramming. Combining attributes with assertions opens other
research areas such as the specification of temporal constraints,
component coordination, and synchronization of multithreading
applications. We are exploring those areas. More contributions would
be very welcome.
References
