Welcome!

Microsoft Cloud Authors: Janakiram MSV, Yeshim Deniz, David H Deans, Andreas Grabner, Stackify Blog

Related Topics: Microsoft Cloud

Microsoft Cloud: Article

Including Assertions in .NET Assemblies

Including Assertions in .NET Assemblies

.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.

Introduction
Bertrand Meyer included the assertion formalism in Eiffel under his Design by Contract metaphor. Works for other languages such as Java and C++ recognize the significance of assertions. This article introduces assertions in .NET code through attributes. This approach changes neither .NET languages nor .NET compilers.

The resulting asserted assembly will have two advantages:
1. To serve as a documentation vehicle: Because assertions are inserted as attributes, they are formal metadata integrated into the assembly.
2. To increase the developer's trust in the assembly: Because assertions can be checked and monitored at runtime by means of reflection, the developer can verify that the assembly really does what the assertions say it does.

Components in Previous Technologies
Technologies like CORBA and COM use IDLs (Interface Definition Languages), but these IDLs do not include more semantic information than that which can be deduced from types, methods, and parameter names.

Java technology alleviates this drawback, but has the following weaknesses:

  • The monolinguistic approach. A Java component can be used only by another Java component. There is no seamless and comfortable way to connect an EJB component to a component developed in another language and vice versa.
  • The documentation extracted from a component consists only of type signatures and comments.
  • The Java reflection mechanism is unable to recover the "information" embedded as comments. Developers must work directly with the internals of the Java bytecode files.

    Strengths of .NET Assemblies
    .NET components are supported by assemblies.

  • A .NET assembly is language neutral. It can be used transparently from any other .NET assembly, independently of the source languages that produced each.
  • A .NET assembly contains code, data, and metadata. Metadata can be fully extracted using .NET reflection capabilities.
  • .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

  • Beugnard, A., Jézéquel, J.M., Plozeau, N., Watkins, D. (1999). "Making Components Contract Aware." Computer. July.
  • Coira, J., Katrib, M. (1997). "Improving Eiffel Assertions Using Quantified Iterators." Journal of Object Oriented Programming. Nov./Dec.
  • eXtensibleC# (XC#): www.resolvecorp.com
  • Design by Contract for Java Using JMSAssert: www.mmsindia.com/DBCForJava.html
  • Fernandez, D., Katrib, M., Pimentel, E. (1999). "Synchronizing Java Threads Using Assertions." Proceedings of TOOLS 31st. IEEE Computer Society.
  • Katrib, M., Martínez, I. (1993). "Collections and Iterators in Eiffel." Journal of Object Oriented Programming. Nov./Dec.
  • iContract: The Java Design by Contract Tool: Click Here!
  • Meyer, B. (1992). "Applying Design by Contract." Computer. IEEE. October.
  • Meyer, B. (1997). Object-Oriented Software Construction. 2nd Edition. Prentice Hall.
  • Meyer, B. (1992). Eiffel: The Language. Prentice Hall.
  • Java with Assertions: http://theoretica.informatik.uni-oldenburg.de/~jawa
  • Support for Assertions in the Rotor Runtime: www.csse.monash.edu.au/~namtt/rotor/MonashRotorProject.html
  • More Stories By Miguel Katrib

    Miguel Katrib is a PhD and a professor in the Computer Science Department at the University of Havana. He is also the head of the WEBOO group dedicated to Web and object-oriented technologies. Miguel is also a scientific advisor in .NET for the software enterprise CARE Technologies, Denia, Spain.

    More Stories By Erich Ledesma

    Erich Ledesma is an undergraduate and student assistant in the
    Computer Science Department at the University of Havana and is a
    student member of the WEBOO group. He has won several prizes in
    student competitions. Erich's main interests are compiling
    techniques, and network and Web programming.

    More Stories By Leonardo Paneque

    Leonardo Paneque is an undergraduate student in the Computer Science
    Department at the University of Havana and is a student member of the
    WEBOO group. His main interests are security, Windows, and GUI
    programming.

    Comments (0)

    Share your thoughts on this story.

    Add your comment
    You must be signed in to add a comment. Sign-in | Register

    In accordance with our Comment Policy, we encourage comments that are on topic, relevant and to-the-point. We will remove comments that include profanity, personal attacks, racial slurs, threats of violence, or other inappropriate material that violates our Terms and Conditions, and will block users who make repeated violations. We ask all readers to expect diversity of opinion and to treat one another with dignity and respect.


    @ThingsExpo Stories
    WebRTC is great technology to build your own communication tools. It will be even more exciting experience it with advanced devices, such as a 360 Camera, 360 microphone, and a depth sensor camera. In his session at @ThingsExpo, Masashi Ganeko, a manager at INFOCOM Corporation, introduced two experimental projects from his team and what they learned from them. "Shotoku Tamago" uses the robot audition software HARK to track speakers in 360 video of a remote party. "Virtual Teleport" uses a multip...
    SYS-CON Events announced today that Telecom Reseller has been named “Media Sponsor” of SYS-CON's 22nd International Cloud Expo, which will take place on June 5-7, 2018, at the Javits Center in New York, NY. Telecom Reseller reports on Unified Communications, UCaaS, BPaaS for enterprise and SMBs. They report extensively on both customer premises based solutions such as IP-PBX as well as cloud based and hosted platforms.
    Coca-Cola’s Google powered digital signage system lays the groundwork for a more valuable connection between Coke and its customers. Digital signs pair software with high-resolution displays so that a message can be changed instantly based on what the operator wants to communicate or sell. In their Day 3 Keynote at 21st Cloud Expo, Greg Chambers, Global Group Director, Digital Innovation, Coca-Cola, and Vidya Nagarajan, a Senior Product Manager at Google, discussed how from store operations and ...
    In his session at 21st Cloud Expo, Carl J. Levine, Senior Technical Evangelist for NS1, will objectively discuss how DNS is used to solve Digital Transformation challenges in large SaaS applications, CDNs, AdTech platforms, and other demanding use cases. Carl J. Levine is the Senior Technical Evangelist for NS1. A veteran of the Internet Infrastructure space, he has over a decade of experience with startups, networking protocols and Internet infrastructure, combined with the unique ability to it...
    Gemini is Yahoo’s native and search advertising platform. To ensure the quality of a complex distributed system that spans multiple products and components and across various desktop websites and mobile app and web experiences – both Yahoo owned and operated and third-party syndication (supply), with complex interaction with more than a billion users and numerous advertisers globally (demand) – it becomes imperative to automate a set of end-to-end tests 24x7 to detect bugs and regression. In th...
    "Cloud Academy is an enterprise training platform for the cloud, specifically public clouds. We offer guided learning experiences on AWS, Azure, Google Cloud and all the surrounding methodologies and technologies that you need to know and your teams need to know in order to leverage the full benefits of the cloud," explained Alex Brower, VP of Marketing at Cloud Academy, in this SYS-CON.tv interview at 21st Cloud Expo, held Oct 31 – Nov 2, 2017, at the Santa Clara Convention Center in Santa Clar...
    "There's plenty of bandwidth out there but it's never in the right place. So what Cedexis does is uses data to work out the best pathways to get data from the origin to the person who wants to get it," explained Simon Jones, Evangelist and Head of Marketing at Cedexis, in this SYS-CON.tv interview at 21st Cloud Expo, held Oct 31 – Nov 2, 2017, at the Santa Clara Convention Center in Santa Clara, CA.
    SYS-CON Events announced today that Evatronix will exhibit at SYS-CON's 21st International Cloud Expo®, which will take place on Oct 31 – Nov 2, 2017, at the Santa Clara Convention Center in Santa Clara, CA. Evatronix SA offers comprehensive solutions in the design and implementation of electronic systems, in CAD / CAM deployment, and also is a designer and manufacturer of advanced 3D scanners for professional applications.
    "MobiDev is a software development company and we do complex, custom software development for everybody from entrepreneurs to large enterprises," explained Alan Winters, U.S. Head of Business Development at MobiDev, in this SYS-CON.tv interview at 21st Cloud Expo, held Oct 31 – Nov 2, 2017, at the Santa Clara Convention Center in Santa Clara, CA.
    "IBM is really all in on blockchain. We take a look at sort of the history of blockchain ledger technologies. It started out with bitcoin, Ethereum, and IBM evaluated these particular blockchain technologies and found they were anonymous and permissionless and that many companies were looking for permissioned blockchain," stated René Bostic, Technical VP of the IBM Cloud Unit in North America, in this SYS-CON.tv interview at 21st Cloud Expo, held Oct 31 – Nov 2, 2017, at the Santa Clara Conventi...
    SYS-CON Events announced today that CrowdReviews.com has been named “Media Sponsor” of SYS-CON's 22nd International Cloud Expo, which will take place on June 5–7, 2018, at the Javits Center in New York City, NY. CrowdReviews.com is a transparent online platform for determining which products and services are the best based on the opinion of the crowd. The crowd consists of Internet users that have experienced products and services first-hand and have an interest in letting other potential buye...
    It is of utmost importance for the future success of WebRTC to ensure that interoperability is operational between web browsers and any WebRTC-compliant client. To be guaranteed as operational and effective, interoperability must be tested extensively by establishing WebRTC data and media connections between different web browsers running on different devices and operating systems. In his session at WebRTC Summit at @ThingsExpo, Dr. Alex Gouaillard, CEO and Founder of CoSMo Software, presented ...
    Leading companies, from the Global Fortune 500 to the smallest companies, are adopting hybrid cloud as the path to business advantage. Hybrid cloud depends on cloud services and on-premises infrastructure working in unison. Successful implementations require new levels of data mobility, enabled by an automated and seamless flow across on-premises and cloud resources. In his general session at 21st Cloud Expo, Greg Tevis, an IBM Storage Software Technical Strategist and Customer Solution Architec...
    A strange thing is happening along the way to the Internet of Things, namely far too many devices to work with and manage. It has become clear that we'll need much higher efficiency user experiences that can allow us to more easily and scalably work with the thousands of devices that will soon be in each of our lives. Enter the conversational interface revolution, combining bots we can literally talk with, gesture to, and even direct with our thoughts, with embedded artificial intelligence, whic...
    To get the most out of their data, successful companies are not focusing on queries and data lakes, they are actively integrating analytics into their operations with a data-first application development approach. Real-time adjustments to improve revenues, reduce costs, or mitigate risk rely on applications that minimize latency on a variety of data sources. In his session at @BigDataExpo, Jack Norris, Senior Vice President, Data and Applications at MapR Technologies, reviewed best practices to ...
    An increasing number of companies are creating products that combine data with analytical capabilities. Running interactive queries on Big Data requires complex architectures to store and query data effectively, typically involving data streams, an choosing efficient file format/database and multiple independent systems that are tied together through custom-engineered pipelines. In his session at @BigDataExpo at @ThingsExpo, Tomer Levi, a senior software engineer at Intel’s Advanced Analytics gr...
    When talking IoT we often focus on the devices, the sensors, the hardware itself. The new smart appliances, the new smart or self-driving cars (which are amalgamations of many ‘things’). When we are looking at the world of IoT, we should take a step back, look at the big picture. What value are these devices providing? IoT is not about the devices, it’s about the data consumed and generated. The devices are tools, mechanisms, conduits. In his session at Internet of Things at Cloud Expo | DXWor...
    Everything run by electricity will eventually be connected to the Internet. Get ahead of the Internet of Things revolution. In his session at @ThingsExpo, Akvelon expert and IoT industry leader Sergey Grebnov provided an educational dive into the world of managing your home, workplace and all the devices they contain with the power of machine-based AI and intelligent Bot services for a completely streamlined experience.
    SYS-CON Events announced today that Synametrics Technologies will exhibit at SYS-CON's 22nd International Cloud Expo®, which will take place on June 5-7, 2018, at the Javits Center in New York, NY. Synametrics Technologies is a privately held company based in Plainsboro, New Jersey that has been providing solutions for the developer community since 1997. Based on the success of its initial product offerings such as WinSQL, Xeams, SynaMan and Syncrify, Synametrics continues to create and hone inn...
    SYS-CON Events announced today that Google Cloud has been named “Keynote Sponsor” of SYS-CON's 21st International Cloud Expo®, which will take place on Oct 31 – Nov 2, 2017, at the Santa Clara Convention Center in Santa Clara, CA. Companies come to Google Cloud to transform their businesses. Google Cloud’s comprehensive portfolio – from infrastructure to apps to devices – helps enterprises innovate faster, scale smarter, stay secure, and do more with data than ever before.