[Fortress-interest] 32bit Integers and Contracts

[Jan-Willem Maessen]

On Jan 18, 2007, at 6:28 PM, Alex Battisti wrote:

> 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:

[factorial with classic int overflow]

> ./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).

As the README notes, throw and catch aren't implemented yet.  Thus we  
haven't put in place all the necessary checking, either.  I'll  
clarify this issue in the README.

> 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.

Hmm, these are indeed not yet implemented, but the README doesn't  
seem to mention that fact.  For the moment I'll fix the README.

> 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.:

Hmm, we just checked in a bunch of changes to this script; I'll try  
to fix the README as appropriate.

Thanks for the trouble reports.  And do rest assured that we're at  
work implementing the not-yet-implemented stuff.

-Jan

>
> 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 "$@"
> _______________________________________________
> Fortress-interest mailing list
> Fortress-interest@experimentalstuff.com
> http://www.experimentalstuff.com/mailman/listinfo/fortress-interest