[Fortress-interest] 32bit Integers and Contracts

[Alex Battisti]

Hello,

when playing around with the following script (using revision 93 from
the svn with Java 1.5 and 1.6 on OS X) I ran into some issues, and do
not know if their are known/expected behavior or bugs:

(* start test.fss *)
component Test
export Executable

run(args:String...) = do
  print factorial(33) " result (33)\n"
  print factorial(34) " result (34)\n"
end

factorial(n:ZZ32):ZZ32
    = if n = 0 then 1
      else n factorial(n-1)
      end

end
(* end test.fss *)

which resulted in:

./fortress test.fss
Parsing test.fss with the Rats! parser: 307 milliseconds
Read /Users/alex/Projects/fortress/ProjectFortress/FortressLibrary.jst:
242 milliseconds
-2147483648 result (33)
0 result (34)
finish runProgram
952 milliseconds

I was expecting an " IntegerOverflowException " (according to the
Fortress Specification page 134).



trying to use contracts like:

(* start test2.fss *)
component Test2
export Executable

run(args:String...) = print "test2\n"

factorial(n:ZZ32):ZZ32
    requires n > 0
    ensures result > 0
    = if n = 0 then 1
      else n factorial(n-1)
      end

end
(* end test2.fss *)

results in:

 ./fortress test2.fss
  test2.fss:8:13: whitespace expected
Parsing test2.fss with the Rats! parser: 314 milliseconds
FAIL: Syntax error.

Any help would be highly appreciated,

thanks
Alex Battisti



p.s. i had to update the fortress script
(fortress/ProjectFortress/fortress) from revision 93 to include
dstm2.jar and bcel-5.2.jar, (the README too seems to be obsolete)
i.e.:

changing:

java -cp "build:third_party/xtc/xtc.jar:third_party/FJ/concurrent.jar" \
com.sun.fortress.interpreter.drivers.fs "$@"

to:

java -cp "build:third_party/xtc/xtc.jar:third_party/FJ/concurrent.jar:third_party/dstm2/dstm2.jar:build:third_party/bcel/bcel-5.2.jar"
\
com.sun.fortress.interpreter.drivers.fs "$@"