FOPSV12MAR2008
Second Embedded Version which parses temporal specs
Final overly parenthesized version (19MAR2008)
FOPSV19MAR2008
Third Initial Embedded Version (IEV3) which parses temporal specs
First Embedded Version which parses temporal specs
(IEV5) Made common superclass of jmlSpecQuantifiedExpressionRest & newly added temporal stuff and added file names to Makefile
Fourth Initial Embedded Version (IEV4) which parses temporal specs
Made common superclass of jmlSpecQuantifiedExpressionRest & newly added temporal stuff and added file names to Makefile
Temporal RAC (04DEC08): Support for never with update methods to make it similar to handling of always, eventually.
Temporal RAC (03DEC2008): Added RAC for a sequence of events.
Temporal RAC: Allowed multiple temporal formulas per type
Temporal RAC Ver 3 (03OCT08): Added never
Now will try to restore jmlrac sanity
Typechecking Version 1
Temporal Test Cases V1
Temporal typechecking Version 3
Temporal test cases V2
Temporal typechecking Version 2
Temporal RAC Ver. 1
Temporal Typechecking Tests Version 1
Sanity restored in jmlrac before trying temporal RAC. Problems: 1) org.jmlspecs.checker/testcase/typecheck: test failed for Primitive_bigint_basic.java 2) org.jmlspecs.jmldodc: make runtests error
Temporal RAC Ver. 2
Temporal RAC Ver. 6 (30OCT08): Turn temporal formula checking on/off for JmlTemporalUnlessExpression (without after, before, etc.)
Temporal RAC (21NOV08): Generalized trace property implementation
Temporal RAC (12NOV2008): First attempt at translating recursive temporal formulas. Added rule for temporal after.
Temporal RAC (15NOV2008_2): First attempt at implementing temporal construct 'Eventually'.
Temporal RAC Ver. 4 (30OCT08): Restored sanity after introducing temporal specification variables per method.
Temporal RAC (15NOV2008): 'Eventually' implementation version 2. Still for only one temporal formula per type and only one eventually occurrence in that formula. Will need to generate multiple methods with different names to allow multiple eventually-traceprops per formula
Temporal RAC (18NOV08): Corrected eventually trace property code generation.
Temporal RAC (14NOV08): Corrected some typechecking by adding a type for trace properties; also misc. RAC code. other than AtMost, Eventually.
Temporal RAC (13NOV08): Corrected static signature generation for temporal events method. Added some typechecking to rule for unless,until to disallow non-trace properties. But this & similar issues need to be dealt with by assigning types instead of manually checking the type of underlying expression using instanceof.
Temporal RAC (15NOV2008_3): First attempt at implementing temporal construct 'Eventually'.
Temporal RAC (15NOV2008): First attempt at implementing temporal construct 'Eventually'.
Temporal RAC (05DEC2008): Added RAC code to check until-related events do occur eventually.
Conjunction/Disjunction of Enabled/NotEnabled ops
Temporal RAC (21DEC08): Basic temporal machine unless implementation.
Temporal RAC: Code in WrapperMethod to call checkTemporalFormula in pre-state of a method.
Readable 'bad events' message instead of modified method signature string.
Give detailed temporal event descriptions in temporal specification errors.
RAC(10Feb09): First enabled/notenabled construct implementation
Temporal RAC (15DEC08): some observer code in temporal state machine
Temporal RAC (30DEC08): Added temporal machine code for atmost formulas
Temporal RAC: JMLTemporalSpecificationError added and other Misc changes.
Temporal RAC (11DEC08): Initial temporal state machine code
Temporal RAC: Reason why some states in temporal machine are non-accepting. Also, (much of the) code for finding full event names moved to JmlTemporalEvent.java
Temporal RAC: Code for between formulas in state machine. Also, code for series of events in a JmlTemporalEvent in the machine builder.
Temporal RAC (13DEC08): Machine code generator before minus actual trace property checking
Temporal RAC: Accepting states for temporal machine.
Temporal RAC (19DEC08): Temporal state machine updates on trace properties.
Support static and *instance* temporal formulas.
Allow enabled/notenabled state props. inside only always traceprops. Fixed nonfinal state enabled/notenabled stateprop violation detection problem.
Temporal RAC (25DEC08 :-)): Added observer pattern implementation using an interface called -- (suprize) TemporalObserver with method update()
Misc. small changes -- (probably) typechecking.
Attempted correction of Primitive_Bigint_Basic.java test failure. Need to know which tokens are of type CToken. Error remains, but modification causes no change otherwise.
RAC(9Feb09): First enabled/notenabled construct implementation
Temporal RAC (13DEC08): Machine code generator before minus actual trace property checking
Temporal RAC: Accepting states for temporal machine.
Static/instance temporal formulas
Temporal RAC: Error messages when machine ends up in non-accepting state
Temporal RAC (21DEC08): State machine before code added
Temporal formulas nullity checks during translation
Temporal RAC (21DEC08): Basic temporal machine unless implementation.
Temporal RAC (15DEC08): some observer code in temporal state machine
Temporal RAC: Minor changes -- removed redundant data, etc
Temporal RAC (11DEC08): State machine code for trace props.
Temporal RAC (18DEC08): Basic temporal machine mechanism
RAC: Changes to static/instance temporal spec implementation.
Changes to state machine accepting state mechanism due to newly added temporal state properties.
Temporal RAC: Minor changes -- removed redundant data, etc
FH (26DEC08): Removed bad import referencing jmlrac/ from checker/JmlTemporalEvent.java
Latest files in temporalspec dir.
cleanup.
Removed bug: Trace properties inside static (instance) temporal formulas need to be (and now are) represented by static (instance) fields
Installation information in readme files
updated temporaljmlc installation instructions.
-- Added visitCatchClause(JCatchClause) to TransMethodBody.java. This allows JML annotations inside the catch block to be translated. -- General cleanup for consistency.
modified install instructions. file
Updated readme.
Removed bug: Trace properties inside static (instance) temporal formulas need to be (and now are) represented by static (instance) fields
Removed redundant directory org.jmlspecs.temporalspecs.
Removed until/unless temporal formula bug (see /home/faraz/Software/JML2/org/jmlspecs/temporalspec/traceprop). General cleanup. Readme files on temporal extension to jml.
Added $ tag in install instructions file.
Install tips, papers on temporaljml included
Added visitCatchClause(JCatchClause) to TransMethodBody.java. This allows JML annotations inside the catch block to be translated.
Updated readme.
temporaljmlc in SEFM '10
updated install temporaljmlc page with upcoming release version number.
correction to TemporalSpecBankAC.java suggested by Bas Wegh
updated install temporaljml with new revision number and added Id to sefm10s readme.