team-worthwhile/worthwhile — Issue #96: Field access of primitive return value is valid
Author: bafain
Created: 2012-02-24 01:37:22+00:00
State: open
Labels: parser / validator / typesystem

Validate the following function definition in Worthwhile and observe that it is valid although `fun` returns primitive Integer value and the postcondition accesses the return value by index.

function Integer fun()
_ensures _return[0] = 0
{
return 0
}