Skip to content

Commit

Permalink
Merge branch 'master' into highprecision
Browse files Browse the repository at this point in the history
  • Loading branch information
@nickbattle
nickbattle committed Oct 18, 2024
2 parents 676e674 + 4310b6e commit a611a56
Show file tree
Hide file tree
Showing 39 changed files with 341 additions and 132 deletions.
3 changes: 2 additions & 1 deletion vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedStatement.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@
import com.fujitsu.vdmj.po.statements.POStatement;
import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.POGState;
import com.fujitsu.vdmj.pog.ProofObligationList;
import com.fujitsu.vdmj.typechecker.Environment;

Expand All @@ -53,7 +54,7 @@ public String toString()
}

@Override
public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env)
public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
{
annotation.poBefore(this, ctxt);
ProofObligationList obligations = statement.getProofObligations(ctxt, null, env);
Expand Down
3 changes: 2 additions & 1 deletion vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POClassInvariantDefinition.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor;
import com.fujitsu.vdmj.po.expressions.POExpression;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.ProofObligation;
import com.fujitsu.vdmj.pog.ProofObligationList;
import com.fujitsu.vdmj.pog.StateInvariantObligation;
import com.fujitsu.vdmj.tc.lex.TCNameToken;
Expand Down Expand Up @@ -68,7 +69,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment

if (!classDefinition.hasConstructors)
{
list.add(new StateInvariantObligation(this, ctxt));
list.add(new StateInvariantObligation(this, ctxt).markUnchecked(ProofObligation.UNCHECKED_VDMPP));
}

return list;
Expand Down
28 changes: 5 additions & 23 deletions vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitOperationDefinition.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,11 +35,11 @@
import com.fujitsu.vdmj.po.expressions.POExpression;
import com.fujitsu.vdmj.po.patterns.POPattern;
import com.fujitsu.vdmj.po.patterns.POPatternList;
import com.fujitsu.vdmj.po.statements.POSimpleBlockStatement;
import com.fujitsu.vdmj.po.statements.POStatement;
import com.fujitsu.vdmj.pog.OperationPostConditionObligation;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.POFunctionDefinitionContext;
import com.fujitsu.vdmj.pog.POGState;
import com.fujitsu.vdmj.pog.POImpliesContext;
import com.fujitsu.vdmj.pog.POOperationDefinitionContext;
import com.fujitsu.vdmj.pog.ParameterPatternObligation;
Expand Down Expand Up @@ -163,25 +163,18 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
obligations.add(new OperationPostConditionObligation(this, ctxt));
}

boolean updatesState = !(body instanceof POSimpleBlockStatement) && body.updatesState();
POGState pstate = new POGState();

if (stateDefinition != null)
{
ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true));
ProofObligationList oblist = body.getProofObligations(ctxt, null, env);
obligations.addAll(body.getProofObligations(ctxt, pstate, env));
ctxt.pop();

if (updatesState)
{
oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE);
}

obligations.addAll(oblist);
}
else if (classDefinition != null)
{
ctxt.push(new POOperationDefinitionContext(this, (precondition != null), classDefinition, true));
ProofObligationList oblist = body.getProofObligations(ctxt, null, env);
ProofObligationList oblist = body.getProofObligations(ctxt, pstate, env);
ctxt.pop();

if (Settings.release != Release.VDM_10) // Uses the obj_C pattern in OperationDefContext
Expand All @@ -192,25 +185,14 @@ else if (precondition != null) // pre_op undefined in VDM++
{
oblist.markUnchecked(ProofObligation.UNCHECKED_VDMPP);
}
else if (updatesState)
{
oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE);
}

obligations.addAll(oblist);
}
else // Flat spec with no state defined
{
ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true));
ProofObligationList oblist = body.getProofObligations(ctxt, null, env);
obligations.addAll(body.getProofObligations(ctxt, pstate, env));
ctxt.pop();

if (updatesState)
{
oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE);
}

obligations.addAll(oblist);
}

if (isConstructor &&
Expand Down
30 changes: 6 additions & 24 deletions vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitOperationDefinition.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,14 +37,14 @@
import com.fujitsu.vdmj.po.patterns.POPatternList;
import com.fujitsu.vdmj.po.statements.POErrorCaseList;
import com.fujitsu.vdmj.po.statements.POExternalClauseList;
import com.fujitsu.vdmj.po.statements.POSimpleBlockStatement;
import com.fujitsu.vdmj.po.statements.POStatement;
import com.fujitsu.vdmj.po.types.POPatternListTypePair;
import com.fujitsu.vdmj.po.types.POPatternListTypePairList;
import com.fujitsu.vdmj.po.types.POPatternTypePair;
import com.fujitsu.vdmj.pog.OperationPostConditionObligation;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.POFunctionDefinitionContext;
import com.fujitsu.vdmj.pog.POGState;
import com.fujitsu.vdmj.pog.POImpliesContext;
import com.fujitsu.vdmj.pog.POOperationDefinitionContext;
import com.fujitsu.vdmj.pog.ParameterPatternObligation;
Expand Down Expand Up @@ -190,54 +190,36 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment

if (body != null)
{
boolean updatesState = !(body instanceof POSimpleBlockStatement) && body.updatesState();
POGState pstate = new POGState();

if (stateDefinition != null)
{
ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true));
ProofObligationList oblist = body.getProofObligations(ctxt, null, env);
obligations.addAll(body.getProofObligations(ctxt, pstate, env));
ctxt.pop();

if (updatesState)
{
oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE);
}

obligations.addAll(oblist);
}
else if (classDefinition != null)
{
ctxt.push(new POOperationDefinitionContext(this, (precondition != null), classDefinition, true));
ProofObligationList oblist = body.getProofObligations(ctxt, null, env);
ProofObligationList oblist = body.getProofObligations(ctxt, pstate, env);
ctxt.pop();

if (Settings.release != Release.VDM_10) // Uses the obj_C pattern in OperationDefContext
{
oblist.markUnchecked(ProofObligation.REQUIRES_VDM10);
}
else if (precondition != null) // pre_op undefined in VDM++
else if (precondition != null) // pre_op state param undefined in VDM++
{
oblist.markUnchecked(ProofObligation.UNCHECKED_VDMPP);
}
else if (updatesState)
{
oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE);
}

obligations.addAll(oblist);
}
else // Flat spec with no state defined
{
ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true));
ProofObligationList oblist = body.getProofObligations(ctxt, null, env);
obligations.addAll(body.getProofObligations(ctxt, pstate, env));
ctxt.pop();

if (updatesState)
{
oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE);
}

obligations.addAll(oblist);
}

if (isConstructor &&
Expand Down
4 changes: 2 additions & 2 deletions vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
{
ProofObligationList obligations = new ProofObligationList();

if (type.isMap(location))
if (!type.isUnknown(location) && type.isMap(location))
{
TCMapType m = type.getMap();
obligations.add(new MapApplyObligation(root, args.get(0), ctxt));
Expand Down Expand Up @@ -144,7 +144,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
}
}

if (type.isSeq(location))
if (!type.isUnknown(location) && type.isSeq(location))
{
obligations.add(new SeqApplyObligation(root, args.get(0), ctxt));
}
Expand Down
7 changes: 4 additions & 3 deletions vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAlwaysStatement.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
import com.fujitsu.vdmj.lex.LexLocation;
import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.POGState;
import com.fujitsu.vdmj.pog.ProofObligationList;
import com.fujitsu.vdmj.typechecker.Environment;

Expand All @@ -51,10 +52,10 @@ public String toString()
}

@Override
public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env)
public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
{
ProofObligationList obligations = always.getProofObligations(ctxt, globals, env);
obligations.addAll(body.getProofObligations(ctxt, globals, env));
ProofObligationList obligations = always.getProofObligations(ctxt, pogState, env);
obligations.addAll(body.getProofObligations(ctxt, pogState, env));
return obligations;
}

Expand Down
5 changes: 4 additions & 1 deletion vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAssignmentStatement.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@
import com.fujitsu.vdmj.po.expressions.POExpression;
import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.POGState;
import com.fujitsu.vdmj.pog.ProofObligationList;
import com.fujitsu.vdmj.pog.StateInvariantObligation;
import com.fujitsu.vdmj.pog.SubTypeObligation;
Expand Down Expand Up @@ -70,7 +71,7 @@ public String toString()
}

@Override
public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env)
public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
{
ProofObligationList obligations = new ProofObligationList();

Expand All @@ -83,6 +84,8 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta

obligations.addAll(target.getProofObligations(ctxt));
obligations.addAll(exp.getProofObligations(ctxt, env));
obligations.stateUpdate(pogState, exp);
pogState.didUpdateState(true);

if (!TypeComparator.isSubType(ctxt.checkType(exp, expType), targetType))
{
Expand Down
8 changes: 6 additions & 2 deletions vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POAtomicStatement.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,8 @@
import com.fujitsu.vdmj.lex.LexLocation;
import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.POGState;
import com.fujitsu.vdmj.pog.POGStateList;
import com.fujitsu.vdmj.pog.ProofObligationList;
import com.fujitsu.vdmj.typechecker.Environment;
import com.fujitsu.vdmj.util.Utils;
Expand All @@ -50,15 +52,17 @@ public String toString()
}

@Override
public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env)
public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
{
ProofObligationList obligations = new ProofObligationList();
POGStateList stateList = new POGStateList();

for (POAssignmentStatement stmt: assignments)
{
obligations.addAll(stmt.getProofObligations(ctxt, globals, env));
obligations.addAll(stmt.getProofObligations(ctxt, stateList.addCopy(pogState), env));
}

stateList.combineInto(pogState); // Delayed effect of every atomic assignment
return obligations;
}

Expand Down
5 changes: 3 additions & 2 deletions vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POBlockStatement.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@
import com.fujitsu.vdmj.po.definitions.PODefinitionList;
import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.POGState;
import com.fujitsu.vdmj.pog.POScopeContext;
import com.fujitsu.vdmj.pog.ProofObligation;
import com.fujitsu.vdmj.pog.ProofObligationList;
Expand All @@ -46,12 +47,12 @@ public POBlockStatement(LexLocation location, PODefinitionList assignmentDefs, P
}

@Override
public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env)
public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
{
ProofObligationList obligations = assignmentDefs.getProofObligations(ctxt, env);

ctxt.push(new POScopeContext());
obligations.addAll(super.getProofObligations(ctxt, globals, env));
obligations.addAll(super.getProofObligations(ctxt, pogState, env));
ctxt.pop();

if (!assignmentDefs.isEmpty())
Expand Down
7 changes: 6 additions & 1 deletion vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@
import com.fujitsu.vdmj.po.expressions.POExpressionList;
import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.POGState;
import com.fujitsu.vdmj.pog.ProofObligationList;
import com.fujitsu.vdmj.tc.lex.TCIdentifierToken;
import com.fujitsu.vdmj.tc.lex.TCNameToken;
Expand Down Expand Up @@ -65,7 +66,7 @@ public String toString()
}

@Override
public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env)
public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
{
ProofObligationList obligations = new ProofObligationList();

Expand All @@ -74,6 +75,10 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta
obligations.addAll(exp.getProofObligations(ctxt, env));
}

// We have to assume the operation call accesses state
pogState.didReadState(true);
pogState.didUpdateState(true);

return obligations;
}

Expand Down
7 changes: 6 additions & 1 deletion vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@
import com.fujitsu.vdmj.po.expressions.POExpressionList;
import com.fujitsu.vdmj.po.statements.visitors.POStatementVisitor;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.POGState;
import com.fujitsu.vdmj.pog.ProofObligationList;
import com.fujitsu.vdmj.tc.lex.TCNameToken;
import com.fujitsu.vdmj.typechecker.Environment;
Expand All @@ -53,7 +54,7 @@ public String toString()
}

@Override
public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, Environment env)
public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
{
ProofObligationList obligations = new ProofObligationList();

Expand All @@ -62,6 +63,10 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POContextSta
obligations.addAll(exp.getProofObligations(ctxt, env));
}

// We have to assume the operation call accesses state
pogState.didReadState(true);
pogState.didUpdateState(true);

return obligations;
}

Expand Down
5 changes: 3 additions & 2 deletions vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCaseStmtAlternative.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@
import com.fujitsu.vdmj.po.patterns.POPattern;
import com.fujitsu.vdmj.pog.POCaseContext;
import com.fujitsu.vdmj.pog.POContextStack;
import com.fujitsu.vdmj.pog.POGState;
import com.fujitsu.vdmj.pog.PONotCaseContext;
import com.fujitsu.vdmj.pog.ProofObligationList;
import com.fujitsu.vdmj.tc.types.TCType;
Expand Down Expand Up @@ -58,12 +59,12 @@ public String toString()
return "case " + pattern + " -> " + statement;
}

public ProofObligationList getProofObligations(POContextStack ctxt, POContextStack globals, TCType type, Environment env)
public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, TCType type, Environment env)
{
ProofObligationList obligations = new ProofObligationList();

ctxt.push(new POCaseContext(pattern, type, cexp));
obligations.addAll(statement.getProofObligations(ctxt, globals, env));
obligations.addAll(statement.getProofObligations(ctxt, pogState, env));
ctxt.pop();
ctxt.push(new PONotCaseContext(pattern, type, cexp));

Expand Down
Loading

0 comments on commit a611a56

Please sign in to comment.