[Oberon] Multiple RETURN in a procedure

[Skulski, Wojciech]

August:

>How do you add your postconditions to a procedure with multiple returns?

What kind of postconditions should I add to the following code? Why do I need any postconditions in this case?

PROCEDURE min (x,y: INTEGER) : INTEGER;
BEGIN IF x < y THEN RETURN (x) ELSE RETURN (y) END END min;



________________________________________
From: Oberon [oberon-bounces at lists.inf.ethz.ch] on behalf of August Karlstrom [fusionfile at gmail.com]
Sent: Sunday, October 23, 2022 10:43 AM
To: oberon at lists.inf.ethz.ch
Subject: [EXT] Re: [Oberon] Multiple RETURN in a procedure

>How do you add your postconditions to a procedure with multiple returns?