Activity for Faraz Hussain
-
Faraz Hussain committed [r9036]
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.
1