#19 VCs corrupted for function operations

[H. Smith]

When an operation returns a value (i.e., is a function) and it's ensure clause is not provided, or is not a single assignment to a variable with the name of the function, VCs are corrupted. So:

Operation Foo() : Integer;
ensures Foo = 5;

Works, but:

Operation Foo(): Integer;

And:

Operation Foo(): Integer;
ensures Foo = 5 and Is_Odd(5)

Will create mal-formed VCs.

[Heather]

I believe this should actually be disallowed. An example like this should be handled by a procedure operation with an extra parameter. Our syntax needs to be updated to disallow this type of ensures clause for a function. (I changed the category to language - that may not be the correct category)