Tidy ApplyExpression and ignore return state changes

nickbattle · Oct 24, 2024 · 1fa92f3 · 1fa92f3
1 parent d0c2b12
commit 1fa92f3
Show file tree

Hide file tree

Showing 2 changed files with 53 additions and 50 deletions.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java
@@ -89,70 +89,72 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 	{
 		ProofObligationList obligations = new ProofObligationList();
 
-		if (!type.isUnknown(location) && type.isMap(location))
+		if (!type.isUnknown(location))
 		{
-			TCMapType m = type.getMap();
-			obligations.add(new MapApplyObligation(root, args.get(0), ctxt));
-			TCType atype = ctxt.checkType(args.get(0), argtypes.get(0));
-
-			if (!TypeComparator.isSubType(atype, m.from))
+			if (type.isOperation(location))
 			{
-				obligations.add(new SubTypeObligation(args.get(0), m.from, atype, ctxt));
+				pogState.didUpdateState();	// Operation calls assumed to update state
 			}
-		}
-
-		if (!type.isUnknown(location) &&
-			(type.isFunction(location) || type.isOperation(location)))
-		{
-			String prename = root.getPreName();
 
-			if (type.isFunction(location) && prename != null && !prename.isEmpty())
+			if (type.isMap(location))
 			{
-				obligations.add(new FunctionApplyObligation(root, args, prename, ctxt));
+				TCMapType m = type.getMap();
+				obligations.add(new MapApplyObligation(root, args.get(0), ctxt));
+				TCType atype = ctxt.checkType(args.get(0), argtypes.get(0));
+
+				if (!TypeComparator.isSubType(atype, m.from))
+				{
+					obligations.add(new SubTypeObligation(args.get(0), m.from, atype, ctxt));
+				}
 			}
 
-			if (type.isOperation(location))
+			if (type.isFunction(location) || type.isOperation(location))
 			{
-				pogState.didUpdateState();	// Operation calls assumed to update state
-			}
-
-			TCTypeList paramTypes = type.isFunction(location) ?
-					type.getFunction().parameters : type.getOperation().parameters;
+				String prename = root.getPreName();
+
+				if (type.isFunction(location) && prename != null && !prename.isEmpty())
+				{
+					obligations.add(new FunctionApplyObligation(root, args, prename, ctxt));
+				}
 
-			int i=0;
-
-			for (TCType at: argtypes)
-			{
-				at = ctxt.checkType(args.get(i), at);
-				TCType pt = paramTypes.get(i);
-
-				if (!TypeComparator.isSubType(at, pt))
+				TCTypeList paramTypes = type.isFunction(location) ?
+						type.getFunction().parameters : type.getOperation().parameters;
+
+				int i=0;
+
+				for (TCType at: argtypes)
 				{
-					obligations.add(new SubTypeObligation(args.get(i), pt, at, ctxt));
+					at = ctxt.checkType(args.get(i), at);
+					TCType pt = paramTypes.get(i);
+
+					if (!TypeComparator.isSubType(at, pt))
+					{
+						obligations.add(new SubTypeObligation(args.get(i), pt, at, ctxt));
+					}
+
+					i++;
 				}
-
-				i++;
 			}
-		}
-
-		if (!type.isUnknown(location) && type.isFunction(location))
-		{
-			if (recursiveCycles != null)	// name is a function in a recursive loop
+
+			if (type.isFunction(location))
 			{
-				/**
-				 * All of the functions in the loop will generate similar obligations,
-				 * so the "add" method eliminates any duplicates.
-				 */
-				for (PODefinitionList loop: recursiveCycles)
+				if (recursiveCycles != null)	// name is a function in a recursive loop
 				{
-					obligations.add(new RecursiveObligation(location, loop, this, ctxt));
+					/**
+					 * All of the functions in the loop will generate similar obligations,
+					 * so the "add" method eliminates any duplicates.
+					 */
+					for (PODefinitionList loop: recursiveCycles)
+					{
+						obligations.add(new RecursiveObligation(location, loop, this, ctxt));
+					}
 				}
 			}
-		}
-
-		if (!type.isUnknown(location) && type.isSeq(location))
-		{
-			obligations.add(new SeqApplyObligation(root, args.get(0), ctxt));
+
+			if (type.isSeq(location))
+			{
+				obligations.add(new SeqApplyObligation(root, args.get(0), ctxt));
+			}
 		}
 
 		obligations.addAll(root.getProofObligations(ctxt, pogState, env));

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POReturnStatement.java
@@ -56,8 +56,9 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 
 		if (expression != null)
 		{
-			obligations.addAll(expression.getProofObligations(ctxt, pogState, env));
-			obligations.stateUpdate(pogState, expression);
+			// Don't process POG state here, because we're returning, so the expression can
+			// have no further effect in the operation.
+			obligations.addAll(expression.getProofObligations(ctxt, new POGState(), env));
 		}
 
 		return obligations;