Added toPattern in state designator

nickbattle · Oct 23, 2024 · d0c2b12 · d0c2b12
1 parent 7d48d6b
commit d0c2b12
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 3 deletions.
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIdentifierDesignator.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POIdentifierDesignator.java
@@ -42,4 +42,10 @@ public String toString()
 	{
 		return name.getName();
 	}
+
+	@Override
+	public String toPattern() throws IllegalArgumentException
+	{
+		return name.getName();
+	}
 }
diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStateDesignator.java b/vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POStateDesignator.java
@@ -45,6 +45,15 @@ public POStateDesignator(LexLocation location)
 
 	@Override
 	abstract public String toString();
+
+	/**
+	 * A pattern, such that "let <pattern> = <exp> in ..." can be used in POs. This
+	 * is not always possible.
+	 */
+	public String toPattern() throws IllegalArgumentException
+	{
+		throw new IllegalArgumentException("Cannot generate pattern for " + this);
+	}
 
 	/**
 	 * @param ctxt

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/ProofObligation.java
@@ -60,6 +60,7 @@ abstract public class ProofObligation implements Comparable<ProofObligation>
 	public static final String BODY_UPDATES_STATE	= "Operation body updates state";
 	public static final String LOOP_STATEMENT		= "Loop modifies state";
 	public static final String HAS_UPDATED_STATE	= "Previous statements updated state";
+	public static final String COMPLEX_ASSIGNMENT	= "Assignment too complex";
 
 	public final LexLocation location;
 	public final POType kind;

diff --git a/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java b/vdmj/src/main/java/com/fujitsu/vdmj/pog/StateInvariantObligation.java
@@ -40,8 +40,15 @@ public StateInvariantObligation(POAssignmentStatement ass, POContextStack ctxt)
 		super(ass.location, POType.STATE_INVARIANT, ctxt);
 		StringBuilder sb = new StringBuilder();
 
-		// Note a StateDesignator is not a pattern, so this may not work!
-		sb.append("let " + ass.target + " = " + ass.exp + " in\n");
+		try
+		{
+			sb.append("let " + ass.target.toPattern() + " = " + ass.exp + " in\n");
+		}
+		catch (IllegalArgumentException e)
+		{
+			// Can't represent designator as a pattern, so cannot check PO
+			markUnchecked(ProofObligation.COMPLEX_ASSIGNMENT);
+		}
 
 		if (ass.classDefinition != null)
 		{
@@ -55,7 +62,7 @@ public StateInvariantObligation(POAssignmentStatement ass, POContextStack ctxt)
 			sb.append(def.invPattern);
 			sb.append(" = ");
 			sb.append(def.toPattern());
-			sb.append(" in ");
+			sb.append(" in\n");
 			sb.append(def.invExpression);
 		}