CDE 1.1 Contract Syntax Specification 

 
 
The current version of the CDE supports the superpositon of contracts on top of Java components. This document presents the way contracts should be edited in order to be correctly "compiled" [Note:1], generated and superposed on top of Java source files.


Contract specification for CDE 1.1

The general format of a contract in the current version of the CDE consists of a mixture of abstract specifications and Java source code sections. This means that Java statements are parsed and generated as defined – the CDE compiler does not detect Java syntax/semantic errors. Therefore, if the code generated by the CDE contains compilation or execution errors, it is very likely that it is not due to a generation error but to mistakes in the Java parts of the contract specification. The Java parts are the ones in which the word Java is used.

contract contractName
participants
  // contract participants
  participant1:Component; //e.g account:Account;
   ...;
  participantn:Component;
attributes
   // private attributes of the contract
   JavaType name1; //e.g double credit;
   ...;
   JavaType namek;
operations
   // private operations of the contract
   //e.g double report_credit_use(){
   //operation body in Java
   //}
coordination
  // rules
 TriggerRuleName:
   when *->> participanti.operation(arguments) && (trigger conditions in Java)
    with (JavaGuardConditions)
    failure{
      //Java guard failure actions
      // throw an exception or return a value
    }
    before{
     //operations to be executed before participanti.operation(arguments)
    };
    do{
     //operations to be executed instead of participanti.operation(arguments)
    };
    after{
     //operations to be executed after participanti.operation(arguments)
    };
 StateConditionRuleName:
    when ?(condition in Java) on
participant1, ..., participantn
    //e.g when ? (checking.getBalance()>min) on checking
    do{
      //set of operations of the participants or the contract
    };
end contract

 

The intuitive semantics of the various constructs is as follows:

  • contract contractName:
    This is the name of the contract as specified by the user when creating a new contract from the CDE menu.

  • participants:
    This is a sequence of formal parameter declarations that identify the classes that become associated through the contract. This sequence can consist of one ore more Java classes that have been added to the current CDE project. Notice that the classes should have been added to the project prior to being declared as contract participants. Otherwise, a compilation error will occur. There are two ways to define participants: either by using the syntax participantName:Class; or by using Class participantName

  • attributes:
    These are the private attributes of the contract. The attributes are generated as written by the user in this section and therefore they have to be specified using Java syntax, for instance double credit;. The contract file generated by the CDE defines, by default, two public methods for each attribute: one to set values and the other to get the current value. For instance, for the attribute double credit; the generated methods would be void setcredit(double _credit){credit = _credit;} to set values to credit, and double getcredit(){return credit;} to get the current value of credit.

  • operations:
    These are private operations of the contract. They should be edited in Java and are generated as specified. Therefore they should be in correct Java syntax and have correct semantics in order to avoid compilation or behaviour errors when integrated in the generated code for the rest of the application. For instance, a Java statement of the form value=3; instead of Value=3; in the operation body will not cause a compilation error in the CDE, but because value is undefined, the generated Java code will give rise to a compilation error. Therefore, it pays off to be careful to use correct Java syntax and semantics in the definition of these operations.

  • coordination:
    This section defines the coordination rules that will be superposed on the participants. There are two types of coordination rules that are currently supported by the CDE: rules on calls to operations of the participants and state condition rules. For more details on the semantics of coordination rules consult the concepts and methodology section of this guide. The syntax of coordination rules consists of either a statement of the form

    when *->> participant.operation(arguments)

    for an operation invocation, or

    when ? (condition in Java) on participant1, ..., participantn

    in case of a state condition rule.

    In the former case, operations that are specified as triggers in rules are called "coordinated" operations. To specify an operation as being "coordinated", it is enough to right-click on the participant class, click on Coordinated Operations on the menu, and use the Selection Dialog to choose the operation. By default, all public operations are specified as coordinated. Notice that participants constructors as well as the Java Object operation toString() cannot be "coordinated".

    The symbol *->> applied to an operation means "any call to that operation". The operation arguments should be consistent, i.e have the same format and name as the ones that are defined in the signature of the operation. For instance, for an operation void Operation(int Amount,double m) defined on a class participant, the rule should be either of the form when *->> participant.Operation(Amount,m) or when *->> participant.Operation(...).

    The && section defines the trigger conditions of the rule, i.e under which conditions the call to the operation constitutes a trigger. In other owords, if the operation is called when this condition is false, the contract will not react. Notice that this section should consist of Java statements placed inside parenthesis.

    The with section defines the guard condition for the trigger: when this condition is false, an exception is raised and a failure is reported to the object that called the operation. This condition should also be written in Java. Once again, it is important to use the correct names for the arguments in the trigger and guard conditions because this may be a source of compilation errors in the generated files. For instance, specifying a condition amount>=100 instead of Amount>=100 for the operation above will not cause a compilation error in the CDE but will cause one when compiling the generated files in Java (amount is not defined). The failure statement for the with guard specifies the Java actions that should be executed in case the guard fails. Because failure is not a Java feature, it is necessary to model the rule failure in case the with condition is false, by either throwing an exception or returning a value to the operation client. Hence, the last statements inside the failure block should be either a throw Exception or a return statement. Because the host language is Java, exceptions that may be thrown should be the ones that are originally declared, if declared, in the signature of the trigger operation. 

    The before, do and after actions of the trigger rule are the ones that are discussed in the contract semantics (see Concepts and Methodology) . Notice that these actions should also consist of Java statements.

    State condition rules are declared by using ? with the condition statement specified inside parenthesis and in Java syntax. The statement, on participant1,participant2,..., is used to declare which participants the rule refers to. For instance, a state condition rule can be of the form

    when ? (participant1.getBalance()>100 && participant2.getBalance()) on participant1,participant2.

    It is important to notice that only statements that do not change the state of the participants may be defined as conditions on state rules. Therefore, when using operations in this section, these should be declared as Queries in the CDE project tree. To do that, it is enough to right click on the operation on the project tree and activate "Query". Finally, it is important to check that only correct Java semantics is incluided in the do section of the rule. A common source of errors is, for instance, having operation invocations in the do sections without  including them in a try-catch block although they are specified as operations that throw Java exceptions.




Note 1: The term "compile" is not used in this document with the concrete meaning of compilation. The compilation action of a contract does not create any byte code whatsoever. It just verifies the correctness of the contract's syntax.

 

 


© Copyright 2001 ATX Software SA. All rights reserved.