Assertions

the three methods have quite different characteristics for static checkers.

assert contains a predicate that needs to be proven.
assume contains an axiom to the checker.
require is like assert but blames the caller of the method.

so, yes, all three are needed.

cheers

Are there any static checkers (existing or in work) that utilize them?     (This is a simple expression of interest in static checkers, not a veiled assertion that if no checkers exist that use the different assert-like methods then there should only be one.)

On Tue, Dec 23, 2008 at 5:09 AM, martin odersky <martin.odersky@epfl.ch> wrote:

the three methods have quite different characteristics for static checkers.

 assert contains a predicate that needs to be proven.
 assume contains an axiom to the checker.
 require is like assert but blames the caller of the method.

so, yes, all three are needed.

cheers

 -- martin


On Tue, Dec 23, 2008 at 6:23 AM, Harshad <harshad.rj@gmail.com> wrote:
> From Predef.scala, I see some redundancies:
>
> def assert(assertion: Boolean) {
>    if (!assertion)
>      throw new java.lang.AssertionError("assertion failed")
>  }
>
>  def assume(assumption: Boolean) {
>    if (!assumption)
>      throw new java.lang.AssertionError("assumption failed")
>  }
>
>  def require(requirement: Boolean) {
>    if (!requirement)
>      throw new IllegalArgumentException("requirement failed")
>  }
>
> Isn't it possible to eliminate these similar functions and reduce name space pollution?
>
> Further, is it not possible to map these to Java's asserts which I believe can be turned on/off at run-time?
>
> cheers,
> Harshad
>
>
>

--
http://erikengbrecht.blogspot.com/

On Tue, Dec 23, 2008 at 3:44 PM, Erik Engbrecht
wrote:
> Are there any static checkers (existing or in work) that utilize them?
>
>
> (This is a simple expression of interest in static checkers, not a veiled
> assertion that if no checkers exist that use the different assert-like
> methods then there should only be one.)

I don't know of any. Gary Leavens once thought about of doing an
analogue of JML, for Scala but I don't know what the status of this
is.

Cheers