> From: Maxim Kizub [mailto:[EMAIL PROTECTED]]
>
> >"Maxim Kizub" <[EMAIL PROTECTED]> writes:
> >
> >> The question was about library support of call-by-contract feature
> >> of the compiler/language.
> >
> >[...]
> >
> >> There should be something more that "more optimized version of core
> >> classes".
> >>
> >> So, are you interested in such kind of cooperation?
> >
> >Assuming the following:
> >
> >1) call-by-contract will not effect run-time speed, and if it does,
> > call-by-contract can be disabled by a compiler switch
>
> First of all, the speed is delayed only by boolean expression
> check, nothing more. Also, compiler tryes to optimize the need
> of checks (for example, if a field was not changed in the method -
> the constraints about this field are not checked on return).
>
> Next, you may manually specify at compile time what kind
> of checks you wish to enable/disable. This includes
> trace calls, asserts, pre/post conditions and invariants, as
> well as line/variable tables generation.
>
> With proper support from JVM (like japhar or kaffe) it may be
> possible to switch these checks on the fly ;-)
>
> >2) GNU Classpath will still be compilable by a `normal' Java compiler
> >
>
> There are some ways to make sources compatible with
> others compilers. The source code included in /*{ ... }*/
> "comments" is ignored by other compilers (since it's a normal
> comment for java) but used as normal source text by
> kiev compiler. So, to use compatible with other compilers way
> we need somthing like this:
>
> class Test {
> int i;
> String s;
> /*{
> invariant CheckSomething {
> i >= 0 :: "Negative i = "+i;
> s != null && s.length() > 0 :: "Empty s";
> }
> }*/
>
> String foo(int j)
> /*{
> require { j > i :: "Too small j <= "+i; }
> ensure { $return != null; }
> }*/
> { return s + i*j; }
> }
>
> If you'll need another way of compatibility syntax - I'll add it.
>
I have many technical problems with the require / ensure thing and its use
in Java.
To make the argument below simpler, I will pretend that Classpath is always
compiled using Kiev and its require/ensure keywords.
Does Kiev optimize methods *assuming* that the requirements are met before
the method is called? Does it optimize the caller based on *assumptions*
about the return value using "ensure"? If it does, there are a number of
very serious problems that could arise.
Consider compiling a Java app against the ordinary Sun library and then
running it on a VM with Classpath installed. Unwarranted assumptions will
be made in Classpath's library (since they aren't checked at the caller),
and the program will not behave as expected.
The other case is when the app is compiled against Classpath and run against
a normal VM. Assumptions may be made about a library method's return value,
and the program, again, will not behave as expected. This one we at least
have control over and can minimize by only using "ensure" when it ensures
exactly the same behavior as Sun, even though we may have better behavior.
Don't get me wrong here, I think ensure / require is a great idea. The only
thing I can think of is some sort of switch in the VM to let Classpath know
not to make assumptions about parameters to public methods and apps know not
to make assumptions about return values from Classpath. This would require
Kiev putting two sets of code into the final code and then having a flag
sitting somewhere that it checks at runtime to figure out whether or not to
make assumptions about the class library's methods. It would, of course,
default to not making assumptions, since that is expected behavior in a
normal VM and that is what writers of non-Kiev apps would want. That would
be messy, but the only way for Kiev-compiled classes to be compatible with
Java. I don't know if you're willing to put in that much work for such a
special case. But I don't see anything we can do on this end.
A question about Kiev that is sort of off-topic: is it possible for me to
write an ensure that *never* generates a runtime check? Say I'm absolutely
certain the return value will work the way I say it does, but I just want to
let the caller know that so that Kiev can do some optimizations (retval !=
null would be a prime example of something like that) after the method call,
such as not checking for NullPointerException.
--John Keiser
