## Statements

In this section, we present the various types of AGREE statements and their uses. Note: Assume Statements (Assume Statements) and Guarantee Statements (Guarantee Statements) exclusively live in component types; while Assert Statements (Assert Statements) and Lemma Statements (Lemma Statements) exclusively live in component implementations.

### Assume Statements

Assume statements specify constraints about a component that are assumed to be true. An example of an assume statement is:

    assume "System input domain" : Input < 10;

The string "System input domain" is used to identify the assumption when performing verification. The expression `Input < 10` expresses the condition that is assumed to hold. When verifying a component implementation, the component’s assumptions are assumed to be true. However, the assumptions of the component implementation’s subcomponents must be proved to hold based on the assumptions of the component and the guarantees of other subcomponents.

### Guarantee Statements

Guarantee statements specify constraints that the component maintains as long as the assumptions have always held. An example of a guarantee statement is:

    guarantee "System output range" : Output < 50;

The string "System output range" is used to identify the guarantee when performing verification. The expression `Output < 50` expresses the condition that is guaranteed to hold.

When verifying a component implementation, guarantee statements are proven by the component assumptions and the guarantees present in subcomponent contracts.

### Equation Statements

Equation statements can be used to create local variable declarations within the body of an AGREE subclause. An example of an equation statement is:

    eq ctr : int = prev(ctr + 1, 0);

In this example, we create a variable that counts up from zero. Variables defined with equation statements can be thought of as ''intermediate'' variables or variables that are not meant to be visible in the architectural model (unlike component outputs or inputs). Equation statements can define variables explicitly by setting the equation equal to an expression immediately after it is defined. Equation statements can also define variables implicitly by not setting them equal to anything, but constraining them with assumption, assertion, or guarantee statements. Equation statements can define more than one variable at once by writing them in a comma delimited list. One might do this to constrain a list of variables to the results of a node statement that has multiple return values or to more cleanly list a set of implicitly defined variables.

### Property Statements

Property statements allow specification of named Boolean expressions. An example property statement is:

    property not_system_start_implies_mode_0 =
    not(OP_CMD_IN.System_Start) > (GPCA_SW_OUT.Current_System_Mode = 0);

Property statements are syntactic sugar (they are equivalent to defining an equation of type bool).

### Constant Statements

Constant statements allow definition of named constants. An example constant statement is:

    const ADS_MAX_PITCH_DELTA: real = 1.0 ;

Identifiers defined by constant statements are used just like equation variables.

### Node Definitions

Node statements are used to define stateful ''functions'' that might be used frequently in a component type or implementation. Nodes can have multiple return values. If this is the cause, they must be referenced by an equation statement that has multiple arguments. Nodes can also be defined in an AADL Package. If so, they can be referenced in any expression anywhere in the model. This way one can make a library of certain types of nodes that are useful for different tasks.

Node definitions in AGREE allow specification of stateful definitions; that is, definitions that can maintain internal state. An example node for maintaining a generalized counter would be:

    node Counter(init: int, incr: int, reset: bool)
    returns (count: int);
    let
        count = if reset then init
            else prev(count, init) + incr;
    tel;

In this example, if reset is true, the counter is reset back to the init value. Otherwise, it increments by incr. The node maintains state (the value of count changes from time step to time step). It is then possible to instantiate this node in other expressions. For example:

    eq x1 : int = Counter(0, 1, prev(x1 = 9, false));

    eq x2 : int = Counter(1, prev(x2, 0),false);

Given these equations, `x1` is a counter that repeatedly counts up to 9 then resets to zero, and `x2` computes the Fibonacci series.

An example of a more complex node with multiple nodes, multiple outputs and local variables would be a 4-bit adder:

    node ADD1(a : bool, b : bool, carry_in : bool)
    returns (out : bool, carry_out : bool);
    let
        out = (a <> b) <> carry\in;
        carry_out = (a and b) or (a and carry_in) or (b and carry_in);
    tel;

    node ADD4 (a0 : bool, a1 : bool, a2 : bool, a3 : bool,
               b0 : bool, b1 : bool, b2 : bool, b3 : bool)
    returns (s0 : bool, s1 : bool, s2 : bool, s3 : bool, carry_out : bool);
    var c0 : bool;
        c1 : bool;
        c2 : bool;
        c3 : bool;
    let
        s0,c0 = ADD1(a0, b0, false);
        s1,c1 = ADD1(a1, b1, c0);
        s2,c2 = ADD1(a2, b2, c1);
        s3,c3 = ADD1(a3, b3, c2);
        carry_out = c3;
    tel;

The ADD1 node takes two single bit inputs and a carry input bit and computes an output and a carry bit. We can use this to create a four-bit adder `ADD4` by "stringing together" four of the one-bit adders. Note that all local variables (defined with var) and all output variables (defined in the returns section) must be assigned exactly one time within the let block.

Note: Nodes cannot be recursive or mutually recursive.

### Record Definitions

Record definitions are used to define record types. Like a struct type in C programming language, a record is a collection of fields, each of its own data type. An example record definition is as follows:

    type foo = struct {a : bool, b : int};

### Real-time Patterns

AGREE also supports the specifications of real-time patterns. These patterns were adopted from the Requirements Specification Language adopted under the CESAR project. Patterns can be used instead of expressions in Assume, Guarantee, or Assert statements. The grammar for the patterns that we support is shown below:

    PatternStatement:
      WheneverStatement
      | WhenStatement
      | RealTimeStatement
      ;

    WhenStatement:
      'when' Expr 'holds' 'during' TimeInterval Expr
      ('exclusively')? 'occurs' 'during' TimeInterval
      ;

    WheneverStatement:
      'whenever' Expr 'occurs' Expr
        ('exclusively')? ('occur' | 'occurs')) 'during' TimeInterval
      | 'whenever' Expr 'occurs' Expr
        ('exclusively')? ('holds') 'during' TimeInterval
      | 'whenever' Expr 'occurs' Expr 'implies' Expr
        ('exclusively')? 'during' TimeInterval
      ;

    RealTimeStatement:
      'condition' Expr 'occurs' 'each' Expr ('with' 'jitter' jitter=Expr)?
      | 'condition' Expr 'occurs' 'sporadic' 'with' 'IAT' Expr
        ('with' '*jitter*' jitter=Expr)?
      ;

    TimeInterval:
      '\[ | (' Expr ',' Expr '\] | )')
      ;

The expressions in each of the patterns must be an IDExpr (a variable without any dots) of Boolean type. Details about the semantics of these patterns, how they are implemented, and how they may be used can be found in the Final Documentation and Technical Report for the Requirements Patterns for Formal Contracts in AADL program.

The time intervals specified by these patterns reference values for a reserved variable named “time”. This variable is present in any counterexamples or inductive counterexamples that the tool produces. Additionally, AGREE contains three special functions that take a single IDExpr as an argument and produce a value of type real. These functions are:

1. timeof(id) – returns the the last value of the variable time in which id was true. If id has never been true then the function returns the value -1.0.

2. timerise(id) – returns the last value of the variable time in which id transitioned to true. If id has never been true then the function returns the value -1.0.

3. timefall(id) – returns the last value of the variable time in which id transitioned to false. If id has never been false then the function returns the value -1.0.

### Advanced Topic: Assert statements

Assert statements allow definition of axioms within the model. Axioms are "facts" about the behavior of the system or the environment that are added to the model to support proofs. An example assertion is of the form:

    assert (FGS_L.LSO.Valid and FGS_R.LSO.Valid) > FGS_L.LSO.Leader = FGS_R.LSO.Leader;

Assertions are sometimes used for architectural patterns whose correctness is established in a separate phase of analysis. The assertion above is from a pattern called leader selection that ensures that one of a set of redundant components is the leader.

Assert statements make unchecked statements about how the component behaves. These are also used to reference variables from a subcomponent in the component contract. For the purpose of analysis assertions are treated just like the system assumptions. However, AGREE never verifies that the assertions actually hold. That is to say, the assertions of a subcomponent are never proven to hold like subcomponent assumptions. Assert statements can refer to equations or features defined in the component type. They are often used to refer to subcomponent variables in contracts higher up in the model hierarchy.

Note: Assert statements are assumed to be true and are not validated in any way by AGREE. Any use of this statement should be exercised with great caution. All assert statements should be examined by a domain expert and formal verification expert.

### Advanced Topic: Lemma Statements

Assert statements are used to introduce lemmas to assist the model checker when performing verification. AGREE uses k-induction over the transition relation to try to prove properties – see Appendix A for a high-level description of the procedure. For many systems and properties, this works very well and is able to prove interesting properties about the system without assistance. However, sometimes a property is true but not provable using this technique. The reason that this happens is the property to be proved is too weak to be inductively provable. Lemma statements are additional properties that are added to an AGREE model in order to strengthen the property to be proved.

An example lemma would be:

    lemma "drug flow lemma" :
        (not drug_flow_stopped) => spo2_never_below_thresh;

From the perspective of proof, lemmas behave the same as guarantees; they must be proven by AGREE. These are used to help the model checker learn facts to improve its ability to prove other properties. However, unlike guarantees, lemmas are not made visible when trying to prove properties at the next level of abstraction. Subcomponent lemmas are not used to prove other subcomponent guarantees or system guarantees.

### Advanced Topic: Linearization Definitions

The linearization definition provides the declaration of a linear approximation of a non-linear expression over segment(s) of its input domain, resulting in a new expression that bounds the non-linear expression with piecewise linear segment(s). The non-linear expression supports a small core of mathematical functions found on a calculator (i.e., '+', '-', '*', '/', '^') and a collection of transcendental mathematical functions. Note: The non-linear expression can contain references to only the input variable (no other AGREE identifiers). Figure 1 demonstrates a linear approximation bounding the output values within the upper and lower bounds.

Figure 1: Bound Non-linear Expression with Piecewise Linear Segments

The following linearization definition example provides the linear approximation for the square operation with a real type input over input interval between -1.0 and 1.0, and input precision of 0.01.

    linearization sq (y : real) over [-1.0 .. 1.0] within 0.01 : y^2.0;

Note: Currently linearization definition with single input of real type is supported.

The following function calls are allowed within the linearization body expression:

> abs, acos, asin, atan, cbrt, cos, cosh, exp, expml, log, log10, log1p, signum, sin, sinh, sqrt, tan, and tanh.