This essay has been submitted by a student. This is not an example of the work written by our professional essay writers.
This report will introduce a method, known as Design by Contract, where a system is viewed as a set of communication components whose interaction is based on defined specifications of mutual obligations --contracts . Furthermore, this report will only focus on DbC for Java by evaluating existing Java DbC tools. It will then identify a suitable tool that provides the main features of DbC (preconditions, postconditions, invariants) followed by further enhancement. The enhancement procedure will include the implementation of a contract semantic reasoner which will ensure that contract conditions are met and at the same time, provide additional useful annotations. Lastly, the DbC tool will be evaluated through means of a case study.
With this project idea in mind, the report aims to enhance an existing DbC tool with DbC features and to investigate the overall approach that DbC can provide for programmers. At the end of iteration, a review will be done to conclude the feasibility of implementing DbC. The review will involve listing the disadvantages and advantages of using DbC, the amount of effort that the programmer requires to use DbC and the complexity of code produced after using DbC.
Context Of Design By Contract
Design by Contract (DbC), originally advocated by Bertrand Meyer, is a software methodology for designing reliable software systems. DbC was originally crafted for the Eiffel language that was developed by him. Subsequently, the concept of DbC has then been extended to many other programming languages such as Java, C#, Groovy and many more. These DbC extensions can now be implemented via third-party support tools.
Retrospectively, DbC has it roots in work with Hoare logic that dates back to Hoare's 1969 paper on formal verification and matured into a powerful way of thinking about software . DbC takes the idea of formal verification and transforms it into a practical programming context.
DbC was developed according to the business contracting metaphor. In the business world, a contract documents precise specifications that define the mutual obligations and benefits between a "client" and a "supplier". In the software world, it describes the relationship between two software components; the client (caller) and the supplier (method). The system specifies a contract of agreement between these two. If the client does not fulfil its end of the contract, the supplier is not obligated to perform its part.  This allows software engineers to embed formal, precise and verifiable specifications (such as invariants, pre and post conditions) for each software components. These specifications contain the semantic information and constraints on each software component, which allows software designers to govern the design and correct use of a class without the need to refer to any external documentation.
DbC aims to improve programming efficiency and software reliability by taking a universal approach to the construction of systems so that they will work correctly at the first time round.
Chapter 2 introduces the fundamental concepts of DbC that are required for the understanding of this report. Thereby, it will consist of background research that involves DbC features (contract, assertions), the range of languages that supports DbC implementation.
Chapter 3 narrows down the research to focus in the context of the Java language. It will introduce the Java assertion facility which is the first step Java towards DbC and the various ways of contract representations that are used in the available DbC third-party support for Java. Next, it will explain the relationship between DbC and Inheritance. Lastly, the how software testing is relevant with DbC.
Chapter 4 introduces Research Methods â€¦..
Chapter 5 introduces Progress â€¦.
Background / Literature Review
This section will introduce a Sorter example (Figure Sorter Example - without contracts) that sort data in Java. This example is used to aid further explanations in later parts of the report. For example, how contract specifications are added onto the Sorter example to implement DbC features.
Figure Sorter Example - without contracts
To start off with this example, we have to assume that the contain the following problems:
An arraylist of integer (ArrayList<Integer> _numbers at Line 7) that is (possibly) out of order
Able to sort this arraylist with a one-time procedure through the sort() method (Line 17)
Able to determine by the isSorted() method (Line 30) to ensure that the arraylist is in the correct order, whereby integer values are arrange in an increasing order.
This example also defines the insertNumber() (Line 21) and removeNumber() (Line 25) method to allow integer values to be added or remove from the arraylist respectively. As for the getNumbers()(Line 13) methods is to return the reference object that is shared between _numbers and numbers arraylist. For further reference of the Sorter example that includes contracts, please refer to Appendix B: Sorter Example.
Contract and Assertions
A (software) system is made of a collection of cooperating components. Design by Contract states that their cooperation should be based on precise specifications - contracts-describing each party's expectation and guarantees. 
A general contract will cover the mutual obligations, benefits and consistency constraints between each party involved. For example, Table Example of a business contract sketches a contract between two parties (mobile owner and mobile service provider) and it shows relationship of how the obligations for each party maps onto a benefit for the other.
Pay monthly bill
Receive mobile services from Supplier
(Mobile service provider)
Provide mobile services stated in the mobile contract
Able to receive prompt payment
Table Example of a business contract
Similarly, the same concept applies to software. A software contract is defined by preconditions (mutual obligation), postconditions (benefits) and invariants (consistency constraint) between classes. This allows a software engineer to specify what a method requires from its caller (client) and guarantees the result after execution. For instance, calling a method it requires both parties to focus on the roles as follows:
Caller: Ensures the precondition(s) of the method holds.
Method: Promises that the work specified in the postcondition will be done and the class invariant still holds after execution
Let take the Sorter constructor (Line 11) from the Sorter example stated in Appendix B: Sorter Example. The contract will be as shown in Table Example of a software contract for the Sorter Constructor in Sort Example (Appendix B: Sort Example).
1.Requires the integer arraylist parameter (numbers) to be valid.
@Pre("numbers!=null") // Pre condition
Allow the client to know that the operation will only change the arraylist that they provide and not a separated arraylist.
1. Ensure there is a valid integer arraylist (_numbers) and this arraylist is equals to the arraylist (numbers) that is passed by the client.
@Invariant("_numbers!=null && getNumbers()==_numbers")
Ensure that a valid arraylist is pass when the constructor is called.
Table Example of a software contract for the Sorter Constructor in Sort Example (Appendix B: Sorter Example)
This contract governs the relationship between both parties. It contains the critical information that can be given about the method. Information such as, what the caller must guarantee to invoke the method and what the caller is entitled to in return.
Contract elements are written as assertions, which are simply Boolean expressions that specify the required logical condition(s) associated with software elements. These conditions are evaluated and required to be true at some point during software execution. Assertions can function as a form of documentation by describing the state a method expects before executing (preconditions), the state of method's result when the execution complete (postconditions) and the state that applies to all instances of the class throughout execution (invariants). This governs the relationship between software components.
Assertions used in DbC are:
Preconditions and Postconditions
Both a precondition and postcondition are associated with a method to provide the semantic specification of the method which acts as an aid in designing it and, later, as an aid to understanding the method from its text.
A precondition expresses the condition that the client must fulfil whenever a method is called to prevent errors. In return, postcondition expresses the condition that the method guarantees at the end of the execution.
An invariant expresses the global properties of every instance of a class, which must be preserved by all methods during runtime. This imposes a general consistency constraint on all methods of the class.
Further information on each assertion will be explained in the next section (). It will provide an example (Appendix B: Sorter Example) to explain how DbC assertions (precondition, postcondition, invariants) are implemented on the Java context.
Design By Contract Assertions In Java
Before contemplating into the implementation of each assertions in Java, it is important to note that methods depicts strong semantic properties, which is independent of any specification.  For example from the list of methods provided in the example (Appendix B: Sorter Example):
sort is only applicable if the arraylist is not null and the number of elements is greater than zero. When method is executed, the return arraylist has to be check if it is sorted in an order.
insertNumber() is only applicable if the arraylist is not null. When method is executed, arraylist size increase by one.
removeNumber() only applicable if the arraylist is not null and the number of elements is greater than zero. When the method is executed, arraylist size decrease by one.
isSorted() is used to verify if the arraylist is sorted correctly after the execution of sort method.
An invariant is a class-level assertion. It specifies the global conditions that must be satisfied by every instance of the class and whenever the instance is externally accessible throughout the runtime. Therefore, an invariant will be implicitly added to both the precondition and postcondition of every exported routine to ensure consistency . If the invariant is violated, it indicates a problem with the class's implementation where a method has changed its state so that it is not consistent.
Figure Example Of An Invariant Declaration in Java
For example (Figure Example Of An Invariant Declaration in Java), the arraylist (_numbers) in the class should always be valid and it should always be the same arraylist parameter (number) that the caller passes through the contractor. If any method is called, it requires the method to ensure that the value of invariant holds during the method execution process.
Furthermore, an invariant reduces code redundancy by linking an attribute and a method, such that it is not required to have an assertion that is repetitively added within a class. For example, if the invariant ("_numbers! =null" ) is not specified , there will be a need to indicated both a precondition (@Pre("_numbers!=null") ) and a postcondition (@Post("_numbers!=null") ) in each method that uses the arraylist (_number ).
A precondition binds the caller of the method: it defines the input condition(s) that the method is imposing on its caller. It is an obligation for the caller and a benefit for the method. Before any execution of the method, the precondition(s) can be evaluated to verify that the caller complies with the conditions. If violated, it is the sign of a bug in the caller.
Figure Example Of Preconditions and Postconditions Declarations In Java
Execute insertNumbers if and only if the input parameter (Integer input) is valid.
Updated arraylist with input item
Ensure updated arraylist contains the input item and arraylist size increased by 1
Table insertNumbers Method Contract Example
For example (Figure Example Of Preconditions and Postconditions Declarations In Javaand Error: Reference source not found), the insertNumbers() method will only be executed if and only if the value of the argument is valid (not null).
A postcondition binds a method: it defines the output condition(s) that characterizes the resulting situation from a successful execution of the method. It is an obligation for the method and a benefit for the caller. Immediately after the execution of the method, the postcondition(s) can be evaluated to verify if the method complies with the conditions. If violated, it is the sign of a bug in the method.
Figure Example Of A Precondition Declaration In Java
For example (Figure Example Of A Precondition Declaration In Java), the sort method should verify with the isSorted() method to ensure that the arraylist is updated. If not, it will return an exception to indicate the bug.
The postcondition includes a special old notation that is only permitted in postcondition. It denotes the value that an expression had on entry to the method. For example (Figure Example Of Preconditions and Postconditions Declarations In Java and Error: Reference source not found), the notation "@Old(_numbers.size())" denotes the arraylist size as captured upon entry of the insertNumbers method. This is to ensure that the method return an updated arraylist that contains the input item and that the arraylist size is increased by 1.
Design By Contract Language Support
This section introduces the range of languages that are available for DbC implementation. Starting with Eiffel language, consist DbC as the foundation, and other related languages either through a native or third-party support.
Eiffel is an ISO-standardized (International Organization for Standardization), object-oriented programming language that was designed by Bertrand Meyer in 1985. There are several definitions that are available. According to the Eiffel Standard ECMA-367," Eiffel is a method of software construction and a language applicable to the analysis, design, implementation and maintenance of software systems" . The details of how Eiffel covers the whole spectrum of software developments will be stated in Appendix C: Eiffel Roles In Software Development Cycle. Although Eiffel is noticeable as a language, it is still known as a method that guides the software engineers through the software development process to attain the productivity and quality of a system. The quality factors involve is reliability, reusability, extendibility, portability and maintainability; these factors are elaborated in Appendix D: Eiffel's Quality Factors. 
After the commencement of DbC, a widespread of new programming languages arises under its influence. These languages implements DbC features either through a native or a third-party support.
These are examples of languages that implements DbC natively:
Ada 2012 
Ada's latest release that extended Ada with contract programming
Ada is an algorithmic-like programming language
Originally created for United States Department of Defence to support modular programming. For now, its mostly used for defence applications.
D Programming Language 
A high level programming language with C-like syntax and static typing.
Provide code reliability features such as unit testing, contract programming  , exception handling and etc. 
Fortress (Sun Microsystems) 
A programming language designed and developed by Sun Microsystems to provide high-performance computing. Oracle Corporation later purchased Sun and it now belongs to Oracle Labs.
Fortress provides DbC feature through the "Function Contracts" which consist of three parts: requires (Precondition), ensures (Postcondition) and invariant. 
A formal language for application programming interface (API) contracts, which extends C# with constructs for non-null types, preconditions, postconditions and object invariants. 
It has a Spec# static program verifier (Boogie) that uses an automatic theorem prover to analyse and verify the contracts. 
Microsoft Visual Studio now supports Spec# compiler.
Vienna Definition Language through Vienna Development Method (IBM) 
A language that make use of formal methods, which are similar to preconditions and postcondition. This stimulates a concept of contracts.
Some well-known applications that implements VDM include:
Dust-Expert: An industrial application of formal methods to determine the safety measures. 
These are examples of languages that implements DbC via a third-party support:
C via DbC for C 
C++ via Digital Mars 
C# and .NET via Code Contracts 
Groovy via GContracts 
Java via Modern Jass , Cofoja , C4J  and many more
AspectJ via Contract4J  and Oval 
Perl via Class:Contract 
PHP via ContractLib 
Python via Python Packages such as Contract for Python  and PyDBC 
Ruby via Contracts.ruby 
These examples, as mention above, are just a small portion of the DbC support that is currently available.
Design By Contract In Java
Although Design By Contract was known as a milestone in software development, however Java does not implement it natively. This section will introduce the different ways of assertions and contract processing that are offered with the range of third-party support. Additionally, DbC assertions will be explained in details through a java Sorter example.
Java Assertion Facility
The assertion facility released in Java 1.4 introduced a new "assert" keyword that allows programmers to include assertions that describes the intended program behavior, which can be checked during runtime . If the assertion is violated, it will raise an exception (java.lang.AssertionError) to indicate that it has failed.
Java provides two way of inserting an "assert" keyword:
The expression is a Boolean expression that is evaluated to determine if it is true or false. If false, it will raise an exception (java.lang.AssertionError) to indicate that it has failed
assert (expression1): expression2
The expression1 is a Boolean expression that is evaluated to determine if it is true or false.
The expression2 is the error message that will be displayed if expression1 raise an exception (java.lang.AssertionError) to indicate that it has failed.
Figure Assert Example: insertNumber method (Sorter Example) with assertion implementation
Figure Assert Exception Example: java.lang.AssertionError with invalid input value
Figure Assert Example: insertNumber method (Sorter Example) with assertion implementation shows the insertNumber() method that made use of the second version of the assert facility (assert (expression1): expression2). If input parameter is given to be null, the assertion will be violated. Therefore it will throw an error as shown in Figure Assert Exception Example: java.lang.AssertionError with invalid input value. The program will return an error that indicates where the error occurs (Line 4) together with the "invalid input" error message and the "null" value that was indicated for the input parameter.
This was a simple yet powerful concept to improve code quality and it shows Java's first step towards design by contract. However the existence of "assert" is still not sufficient to provide a strong format of DbC in Java and it reinforce the perspective that Java will never have native support for DbC. With this perspective, many third-party projects have been created to promote DbC to Java and this will be explained in later segments of the report [Insert Reference].
Ways Of Contracts Representation
A contract basically occurs base on two different approaches; internal or external to source code.
For the former approach, contracts are specified as a kind of annotation within the source code. These annotations are subjected to further transformation that is dependent on the third-party support. For example, different third-party support uses different ways to specify annotation.
The ways of specifying an annotation could be as follow:
Java comments are just line (//) or block-comments (/*â€¦. */) that are normally ignored by the compiler. Java comments requires a Java source parser to analyze the source code to identify comments that represents the contract. For the example of how Java comments is used Jass  to specify contracts, refer to Appendix E: Examples of Contracts Representation.
Javadoc tags are comment-based annotations that require a doclet to process the specified set of tags. These are case-sensitive tags that start with an "at" sign (@) and it must start at the beginning of a line else it is treated as a normal text.
According to the Java Standard Edition Documentation, "Doclets are programs written in the Java programming language that use the doclet API to specify the content and format of the output of the Javadoc tool." . DbC tools could either write their own doclet or customize the Java standard doclet to suit its needs.
For the example of how Javadoc tags are used in Java Modeling Language  to specify contracts, refer to Appendix E: Examples of Contracts Representation.
Java annotations were available since Java Development Kit (JDK) version 1.5. They are created to complement Javadoc tags. In simple terms, if the markup is intended for documentation, it should be a Javadoc; otherwise, it should be an annotation. When the java source code is compiled into class files, the annotation processors will then process the annotation.
Figure Customized Annotation Example: Cofoja Postcondition (@Ensures) 
Figure Java Annotation Example: Precondition and Postcondition used in Cofoja 
DbC features can be created with customized annotations that consist of an at-sign (@) followed by an annotation type and a parenthesized list of element-value pairs which are compile-time constants . For example in the Cofoja tool , it creates a customized annotation "@Ensures" by writing its own annotation (Figure Customized Annotation Example: Cofoja Postcondition (@Ensures) ) with the additional information to declare the annotation parameters.
For example in Figure Customized Annotation Example: Cofoja Postcondition (@Ensures) , these are the list of parameters that are used:
It defines the type of the annotation. @Documented indicates that this annotation is a type that is to be documented by the Javadoc 
Target indicates the kind of program element that the annotation type is applicable. In this case, java.lang.annotation.ElementType.METHOD indicates that this annotation is a method declaration and java.lang.annotation.ElementType.CONSTRUCTOR indicates that this annotation can also be a constructor 
@Retention(..) indiscates how long this annotation can be held.
RententionPolicy.RUNTIME indicates that the compiler wills documents the annotation in the class file and the virtual machine (VM) will retain it at run time.
This shares the similar concept to an interface declaration whereby it is used to declare the class as a new annotation.
With a new declaration of an annotation (Figure Customized Annotation Example: Cofoja Postcondition (@Ensures) ) and an annotation processor, "@Ensures" can be used to define precondition behavior (Figure Java Annotation Example: Precondition and Postcondition used in Cofoja ) during implementation. For information regarding on Java annotation customization, refer to Appendix F: Java Annotations API.
Contracts external to source codes
For the second approach, contracts are specified as an external source code and will be bounded to the actual source code.
Figure Contract external from source code Example with C4J - Sorter Class 
Figure Contract external from source code Example with C4J - Contract class 
For example in C4J, a contract is implemented as a separate class (Figure Contract external from source code Example with C4J - Sorter Class ) and it will be linked to the source code (Figure Java Annotation Example: Precondition and Postcondition used in Cofoja ) at compile time using an annotation (@ContractReference). Within the contract class (Figure Contract external from source code Example with C4J - Sorter Class ) it will state the precondition (pre_insertNumber) and postcondition (post_insertNumber) for insertNumber method. 
Design By Contract And Inheritance
This section will explain why inheritance is central to the DbC paradigm and give an overview of their relationship.
Inheritance And Contracts
Inheritance in DbC appears as a form of subcontracting, a contract that delegates some of the obligations of a prior contract to another party. It has an "is-a" relationship that exists between the caller (client) and method (supplier). Figure A Caller-Method relationship with Inheritance shows the "is-a" relationship where Class B is a subclass of Class A. In order words, Class A subcontracts methods to Class B and any caller that satisfies Class B's specifications also satisfies Class A's specifications.
For example (Figure A Caller-Method relationship with Inheritance), Class B inherits from Class A then:
Every method in Class A is also a method in Class B
Class B inherits the contracts of its parent (Class A), which means
Methods' preconditions and postcondition apply to instances of Class B
Invariants in Class A applied to instances of Class B
Figure A Caller-Method relationship with Inheritance
Inheritance And Assertions
There are basic inheritance rules that are used in DbC to govern the relationship between inheritance and each type of assertions. These rules will be introduced according to each assertion type through the example shown in (Figure A Caller-Method relationship with Inheritance).
Inheritance rule: The invariants of all the parents of a class applied to the class itself 
The invariants of a class are combined (AND- logical conjunction operation) with all invariants of the parent classes to form the invariant for the new class. 
From the example above (Figure A Caller-Method relationship with Inheritance), Class B inherits the invariants stated in Class A. If Class B wants include an invariant x2, it will be added on to x2 and form a new invariant clause ("@Invariant: x1, x2").
Precondition And Postcondition
Precondition Inheritance rule: A precondition of a subclass method has to be equal to or weaker than the original precondition 
Postcondition Inheritance rule: A postcondition of a subclass method has to be equal to or stronger than the original postcondition 
These inheritance rules are required to uphold an "honest" relationship between the caller (client) and method (supplier) when declaring a new method in the subclass. A precondition of the newly declared method is combined with the previous precondition(s) using the logical disjunction operation (OR). As for postconditions, they are combined using the logical conjunction operation (AND).
For example (Figure A Caller-Method relationship with Inheritance), if a new precondition y2 (@Pre("input >=5")) is added onto ClassB.add() and it is stronger than the precondition y1 (@Pre("input >=3")) as stated in ClassA.add(). This will be unfair to caller, as the caller will not know about the new precondition that is needed for Class B. Therefore, it is only fair to expect less (weaker) from the caller than what they are prepared to do. 
Similarly, if a new postcondition z2 (@Post("result >=3")) is added onto ClassB.add() and it is weaker than the postcondition z1 (@Pre("result >=5")) as stated in ClassA.add(), the caller will not receive the expected return that was guaranteed by ClassA.add(). Therefore, it is only fair to deliver a stronger result to the caller than what they expect to get. 
Design By Contract And Software Testing
This section analyses the relationships between DbC and software testing. It will also include a comparison between the correctness and traceability support that both provide.
According to an article published by IEEE Computer Society , the importance of DbC for constructing reliable software has been emphasized after a space rocket explosion due to a $500 million software error. It was an error, which fails to have an explicit exception handler to catch an exception due to a floating-point error: a conversion from a 64-but integer to a 16-bit signed integer. After a list of thorough software testing, the software error was still not detected. This determines that testing can only detect the presence of a defect and not their absence. 
DbC and software testing are complementary and no relevant of them guarantees correctness. Software testing tries to detect defects by uncovering the inconsistencies between implementation and specifications. As for DbC, it tries to prevent defects, through built-in assertions that support executable contract specification, during the design and implementation phase. Software testing detects a wide range of defects whereas DbC prevents specific types of bugs due to the incorrect assumptions between the caller (client) and method (supplier). 
DbC and software testing support traceability. DbC assertions are a way to record requirements in the source code. As for software testing, it maps assertions back to the requirements through regression testing. 
Despite that each of them has a different focus and strong points; there are still overlaps between software testing and DbC. For example, there are various types of software testing that are implemented within DbC environment.
The types of software testing are as follows:
Unit testing is a procedure that is used to validate individual units of source code to ensure that they are working properly. For example, JUnit testing validates individual units of source code by writing test cases with the Java assert facility.
Since both DbC and unit testing address software correctness through the assertion mechanisms it leads to some confusion. Although they intersect, they are still different approaches with different objectives and properties.
Firstly, DbC address correctness for the caller-method relationships. This is to ensure that the caller (client) and the method (supplier) responsibilities are correct. As for unit testing, it addresses correctness of a single method under a specific scenario.
Secondly, DbC does not require external documentation as it is stated within the codes and this does not implies to unit testing.
Lastly, unit testing consist of a set of repeatable test cases that ensure that the consistency of the software is maintained if there is any code modification.
Integration testing is a procedure in which individual units of source code are combined and tested as a group. This is totally different from DbC. However, integration testing is related to DbC as it can verify the contract between the caller (client) and the method (supplier). This will ensure that the precondition and postcondition are working properly together.
Work in Progress
Work in Progress
Appendix A: Glossary
Note: This glossary defines specific terms or abbreviations that have been interpreted in the context of this report.
Design By Contract
In software system, a client is the caller that starts off a method.
In software system, a supplier is the method itself.
International Organization for Standardization
A language in the context of programming.
Application Programming Interface
Java Development Kit
Logical Disjunction operation
Logical Conjunction Operation
An international industry association that is familiarize with standardization of Information and Commendation Technology and Consumer Electronics.
Appendix B: Sorter Example
Sorter class is an example that uses an existing Design By Contract tool. The purpose of this example is to aid explanations of the deliverables that are stated in the report. 
Appendix C: Eiffel Roles In Software Development Cycle
Table Eiffel Roles in Software Development According to Eiffel Tutorial  defines the roles of Eiffel in each software development cycle phase.
Software Development Phase
Eiffel can be used as a descriptive tool to analyze and document the structure and properties of a system
Eiffel can be used to build solid and flexible system structures
Eiffel provides practical and efficient software solutions which is comparable to solutions based on traditional approaches
(e.g. Fortran language, C language)
Eifel provides architectural flexibility of the resulting
Eiffel provides a partial substitute for maintaining software documentation during development. It auto generates documentations (textual and graphical) from the software itself.
Table Eiffel Roles in Software Development According to Eiffel Tutorial 
Appendix D: Eiffel's Quality Factors
These are the list of quality factors that is quoted from the Eiffel Tutorial 
"Reliability: producing bug-free systems, which perform as expected.
Reusability: making it possible to develop systems from prepackaged, high-quality components, and to transform software elements into such reusable components for future reuse.
Extendibility: developing software that is truly soft -- easy to adapt to the inevitable and frequent changes of requirements and other constraints.
Portability: freeing developers from machine and operating system peculiarities, and enabling them to produce software that will run on many different platforms.
Maintainability: yielding software that is clear, readable, well structured, and easy to continue enhancing and adapting. " 
Appendix E: Examples of Contracts Representation
In this appendix, it provides an example for each ways of contract representation that was mention in the previous section (3.1.2).
As shown in Figure Java Comments Example: Precondition and Postcondition used in Jass, this is how Jass  (DbC third-party support) make use of java comments to specify a precondition (require) and a postcondition (ensure). These assertions are enclosed within the block-comments and separated by semicolon into well-defined parts.
Figure Java Comments Example: Precondition and Postcondition used in Jass
The Java Modeling Language (JML)  applies a similar Javadoc concept to defines its JML specifications. JML specifications are written in comment-based annotations with an at-sign (@). These JML specifications use a doclet (jmldoc) to process these pre-defined Javadoc.
As shown in Figure Javadoc Tags Example: Precondition and Postcondition used in Java Modeling Language (JML) , a doclet defines that a "@ ensure" tag represents a postcondition and the content of the tag is then used to create a type that actually implements a postcondition
Figure Javadoc Tags Example: Precondition and Postcondition used in Java Modeling Language (JML) 
Appendix F: Java Annotations API
In this appendix, it contains information that is provided by the Java Annotation API to custom a new annotation. 
These are various types of annotation that can be created
Annotation Types Summary
Indicates that annotations with a type are to be documented by javadoc and similar tools by default.
Indicates that an annotation type is automatically inherited.
Indicates how long annotations with the annotated type are to be retained.
Indicates the kinds of program element to which an annotation type is applicable.
Table Annotation Types constant details From java.lang.annotation API 
These enumerated constant provide a simple classification of the declared elements in a Java program. These can are used with the Target meta-annotation (@Target). 
Enum Constant Summary
Annotation type declaration
Field declaration (includes enum constants)
Â Local variable declaration
Class, interface (including annotation type), or enum declaration
Table The List of ElementType constant details taken from java.lang.annotation API 
These are various policies that can be indicated for retaining annotations. They are used in conjunction with the Retention meta-annotation (@Retention). 
Enum Constant Summary
Annotations are to be recorded in the class file by the compiler but need not be retained by the VM at run time.
Annotations are to be recorded in the class file by the compiler and retained by the VM at run time, so they may be read reflectively.
Â Annotations are to be discarded by the compiler.
Table List of RetentionPolicy constant details taken from java.lang.annotation API 
Appendix G: Project Plan
Project Title: Design Contract In Java Project Period: 1st February 2013 - 6th September 2013
Student Name: Ng Yu Wen
Supervisor: John Sargeant
Identify techniques related to DbC
Identify existing Java DbC tool
Identify suitable DbC tool for comparison
Identify a suitable existing DbC tool for enhancement
Implement a contract syntax/condition validation in the DbC tool
Start Progress Report
Test a contract syntax/condition validation in the DbC tool
Case Study - List advantages/disadvantages of DbC tool usage for the development of a contract syntax/condition validation
Implement a contract semantic reasoner (Part 1)
Finalize Progress Report
Test the contract semantic reasoner
Case Study - List advantages/disadvantages of DbC tool usage for the development a contract semantic reasoner
Implement a contract semantic reasoner (Part 2)
Identify possible new annotations
Implement new annotations to the existing DbC tool
Test the contract semantic reasoner and new annotations
Case Study - List advantages/disadvantages of DbC tool usage for the development of a contract semantic reasoner and new annotations
13th May 2013 -7th June 2013