Evaluation
The evaluation of a rest \? Q proceeds as follows. The path
Q is evaluated. If the result obtained is a failure
$fail(k), where k>0, then the "weakened" failure
$fail(k-1) is taken to be the result of the whole construct. Otherwise,
the result of evaluating Q is taken to be the result of the whole
construct.
The path Q is evaluated at the level m+1, where
m is the level at which the whole construct is evaluated.
Env,m+1,St |- Q => Ge,St'
--------------------------
Env,m,St |- \? Q => Ge,St'
Env,m+1,St |- Q => $fail(0),St'
--------------------------------
Env,m,St |- \? Q => $fail(0),St'
Env,m+1,St |- Q => $fail(k+1),St'
---------------------------------
Env,m,St |- \? Q => $fail(k),St'
Env,m+1,St |- Q => $error(Ge),St'
----------------------------------
Env,m,St |- \? Q => $error(Ge),St'