Stateless and pure

Stateless is first a semantic notion, meaning that a stateless feature does not refer to any state. To show that property to the clients, we add a syntactical notation based on the notion of constants in Eiffel, this looks like:

f (a: STRING): SOME_TYPE =
    do
        create Result.make (a)
        ...
    end

With some validity rules:

• only unqualified calls to stateless features are permitted.

With some validity rules for redefinition:

• once a routine is stateless its redefinitions have to be stateless.
• a stateful routine can become stateless.