Paulo Pinto: > http://www.spark-2014.org/entries/detail/spark-2014-rationale-pre-call-and-pre-loop-values It also explains about the Loop_Entry attribute, useful for loop invariants, neat :-) Bye, bearophile