[Javapathfinder-devel] SF.net SVN: javapathfinder: [738] trunk

[<pcm...@us...>]

Revision: 738
          http://javapathfinder.svn.sourceforge.net/javapathfinder/?rev=738&view=rev
Author:   pcmehlitz
Date:     2008-01-28 21:19:44 -0800 (Mon, 28 Jan 2008)

Log Message:
-----------
start to roll in missing contract extensions, but not yet complete

* model space contracts - still needs some polishing, and needs to be aligned with native properties (with which it
shares the same interface in app/). This also requires @Local to be implemeted, to provide additional safeguards
against contract side effects. It's debatable if the model should be "just call arbitrary user code" or "only
allow very restricted user code" to avoid side effects on the state space. For now, we go with the second one, otherwise
we have to introduce a synthetic wrapper around contracted method calls. The reason is that I see this as a last
measure anyways, and expect the majority of contract types to be built-in or native side

@Local could be a very useful property on its own, think I do this next as a complement to @Const (which also needs
to be integrated into ContractVerifier)

* had to refactor Contract for this, pulling the generic Satisfies to toplevel

* added very minimalistic support for DateFormat parsing

Modified Paths:
--------------
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_SimpleDateFormat.java
    trunk/extensions/statechart/env/jvm/gov/nasa/jpf/jvm/NativeStateMachine.java
    trunk/src/gov/nasa/jpf/jvm/JVM.java
    trunk/src/gov/nasa/jpf/jvm/ThreadInfo.java
    trunk/src/gov/nasa/jpf/test/Contract.java
    trunk/src/gov/nasa/jpf/test/ContractContext.java
    trunk/src/gov/nasa/jpf/test/ContractSpecParser.java
    trunk/src/gov/nasa/jpf/test/Operand.java
    trunk/src/gov/nasa/jpf/tools/ContractVerifier.java
    trunk/test/gov/nasa/jpf/test/TestContracts.java

Added Paths:
-----------
    trunk/app/gov/nasa/jpf/Local.java
    trunk/app/gov/nasa/jpf/Predicate.java
    trunk/env/jvm/gov/nasa/jpf/jvm/JPF_java_text_DateFormat.java
    trunk/src/gov/nasa/jpf/test/Satisfies.java


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.