Pre- and Post- conditions management in functions: a syntax proposal about sarl HOT 7 OPEN

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.

from sarl.

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

from sarl.

We may introduce invariant conditions also:

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

from sarl.

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.

from sarl.

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)\"";
   }
}

from sarl.

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

from sarl.

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

from sarl.