JPO {
int JPO_FILE_FORMAT_VERSION String absolutePath int nbClasses Class classes[nbClasses]
The JPO_FILE_FORMAT_VERSION value for this version is 12. absolutePath corresponds to the absolute path of the .java file corresponding to this jpo file.
Class {
String name ProofObligations staticInitialization int nbConstructors Method constructors[nbConstructors] int nbMethods Method methods[nbMethods]
Method {
String name String signature String pmiName int firstLine ProofObligations proofObligations
ProofObligations {
int nbHypothesis VirtualFormula hypothesis[nbHypothesis] int nbLemmas Lemma lemmas[nbLemmas]
Lemma {
String name int nbHypothesis int hypothesisIndex[nbHypothesis] int nbGoals Goal goals[nbGoals] int nnBox Box boxes[nbBox]
Goal {
int number byte proofState byte proofForce String methodList VirtualFormula goal Formula originalFormula int nbSubstitution Substitution substitutions[nbSubstitution]
Substitution {
byte token union { { String elements Formula newElements } subElements { Formula newArrayLength } subArrayLength { Formula old Formula new } subFormula { Formula newInstances } subInstances { String tmpVar Formula newTmpVar } subTmpVar { Formula typeofLeft Formula typeofRight } subTypeof { Formula old Formula b Formula c Formula d } subMemberField }
VirtualFormula {
int index byte origin Formula f Box b
Box {
int line int column int length byte comment String info
Formula {
int token union { { Formula left Formula right } binaryFormula { QuantifiedVarForm qantifiedVariables Formula body } quantifiedFormula { Formula cond Formula left Formula right } questionFormula { String BText String JavaText } terminalFormula { String BText String JavaText } typeFormula { Formula f } unaryFormula }
QuantifiedVarForm {
Formula variable Formula type boolean hasNext union { { QuantifiedVarForm next } { } }