JavaMOP 1.0 Past Time Linear Temporal Logic with Calls and Returns (JavaPTCaRet) Plugin
This version of JavaMOP is old and not supported anymore! Go to the JavaMOP webpage for the latest version.
This is JavaMOP1.0, which is now deprecated. Go to JavaMOP for the current version. 



...  
...  
...  ...  ...  ...  
...  ...  ...  ...  ...  ...  ...  
MOP Matrix: a clickable map of MOP pages. 
Contents 
Overview
ptCaRet extends the past time linear temporal logic (PTLTL) with call/return atoms. In addition to the standard temporal operators, it also includes abstract variants of past temporal operators, which can express properties over traces in which terminated function or procedure executions are abstracted away into a call and a corresponding return. This way, ptCaRet can express safety properties about procedural programs which cannot be expressed using conventional linear temporal logics.
Input
PTCaRet formulae use the following syntax, which is defined in BNF (extended with the common {p} for zero or more and [p] for zero or one repetitions of p, respectively):
<Formula> ::= "true"  "false"  <Event Name>  <Formula> "and" <Formula>  <Formula> "or" <Formula>
 "not" <Formula>  <Formula> "implies" <Formula> <! Normal boolean constants and operators>
 "(*)" <Formula>  <Formula> "S" <Formula>  "<*>" <Formula>  "[*]" <Formula> <! Standard temporal operators>
 "(*a)" <Formula>  <Formula> "Sa" <Formula>  "<*a>" <Formula>  "[*a]" <Formula> <! abstract temporal operators>
 "@b" <Formula>  "@c" <Formula> <! derived temporal operators: at begin and at call>
 <Formula> "Ss@b" <Formula>  "<*s@b>" <Formula>  "[*s@b]" <Formula> <! derived begin stack operators>
 <Formula> "Ss@c" <Formula>  "<*s@c>" <Formula>  "[*s@c]" <Formula> <! derived call stack operators>
 <Formula> "Ss@bc" <Formula>  "<*s@bc>" <Formula>  "[*s@bc]" <Formula> <! derived beginorcall stack operators>
Unary operators have higher precedence than binary operators. The binary operators in decreasing order of precedence are and > or > implies > S*; here S* includes all the variants of the since operator. Please refer to the corresponding technical report for formal definitions of these operators.
Output
Intermediate Java code used by JavaMOP for the PTCaRet formula specified.
Run the JavaPTCaRetPlugin Online
 Note: The name of the generated Aspect will be the name of the first specification in the text box + MonitorAspect. The name of the .aj file you intend to compile needs to be the same. For example, for LeakingSyncCFG, the generated aspect is LeakingSyncCFGMonitorAspect, and should be placed in a file named LeakingSncCFGMonitorAspect.aj.
 Note: One may append within or !within clauses to the event definitions in JavaMOP to control the scope of instrumentation. For example, if it is certain that some class C will not trigger any event of interest, one may use !within(C) in the event definitions to ignore C during the instrumentation, improving the instrumentation efficiency. The syntax of the within clause can be found in the AspectJ documentation.
Please press the Run button once and wait; it may take a few seconds to run JavaMOP1.0_PTCARET; the execution of JavaMOP1.0_PTCARET using this web interface is limited to 2 minutes of CPU time and 500 MB of RAM.