PVS
PVS copied to clipboard
latex rendering of tables is confused
I've tried two versions of table for gcd. Both render incorrectly.
gcd2(x,y): RECURSIVE posnat =
TABLE
%--------+-------------+-------------++
|[ x = y | x > y | ELSE ]|
%--------+-------------+-------------++
| x | gcd2(x-y,y) | gcd2(x,y-x) ||
%--------+-------------+-------------++
ENDTABLE
MEASURE x+y
has an empty first cell. The one below it contains x
.
gcd2(x,y): RECURSIVE posnat =
TABLE
%-------+-------------++
| x = y | x ||
%-------+-------------++
| x > y | gcd2(x-y,y) ||
%-------+-------------++
| ELSE | gcd2(x,y-x) ||
%-------+-------------++
ENDTABLE
MEASURE x+y
has an additional empty first line that ends "open".