Pre- and Post- conditions management in functions: a syntax proposal

[ngaud]

This is a proposal for the syntax related to functions definition and their associated pre- and post- conditions

def push(s: String, i: Integer) : String
with
pre: not Is_Empty(S), i>0;
post: not Is_Empty(push);
{
//function body
push = myString;
}

<!---
@huboard:{"custom_state":"","order":2.607262565755528e-54,"milestone_order":76.98460230969204}
-->

[gallandarakhneorg]

If the proposed syntax is allowed to return a value from a function, the compiler must avoid local definition of variables of the same name.

[gallandarakhneorg]

The work on this issue should be done at the same time as the one for the issue #55.

[gallandarakhneorg]

We may introduce invariant conditions also:

agent A1 {
    var int i
    with invariant: i>0
}

[gallandarakhneorg]

Currently, the with keyword is already defined. It is used for specifying generic types:

def push(s: A, i: B) with A extends Type1, B extends Type2 {
}

Currently, the generic type definitions could be assimilated to invariants.

[gallandarakhneorg]

Considering the precondition example given by @ngaud. It could be written with the current SARL syntax:

def push(s: String, i: Integer) : String with !Strings::isEmpty(s), i>0 {
   // The code
  null
}

Of course, the SARL compiler must be updated for detecting XExpression associated to the with keyword, and for generating the Java code that corresponds to the pre-condition tests.
I propose to generate the following Java code:

public String push(final String s, final Integer i) {
   assert !Strings.isEmpty(s) : "Invalid pre-condition \"!Strings::isEmpty(s)\"'";
   assert i > 0 : "Invalid pre-condition \"i>0\"'";
   // The code
  return null;
}

Regarding the postcondition, we may define a keyword "post ".

def push(s: String, i: Integer) : String with post Strings::isEmpty(it) {
   // The code
}

The it keyword will be mapped to the returned value in the context of the postcondition.
The generated Java code may be:

public String push(final String s, final Integer i) {
  String $$returnedValue;
   try {
       // The code
       $$returnedValue = null;
      return $$returnedValue;
   } finally {
        final String it = $$returnedValue;
        assert Strings::isEmpty(it) : "Invalid postcondition \"Strings::isEmpty(it)\"";
   }
}

[gallandarakhneorg]

Pre and post conditions should also be used for static validation by the SARL compiler.

[gallandarakhneorg]

This issue in now part of the PhD thesis of @tpiotrow.