Include precondition in generated implementation.

utwente-fmt · Aug 14, 2024 · d53c591 · d53c591
1 parent 77343b4
commit d53c591
Show file tree

Hide file tree

Showing 5 changed files with 29 additions and 10 deletions.
diff --git a/examples/publications/2024/IFM2024VeyMontPermissions/0-TTT/0-TTT.pvl b/examples/publications/2024/IFM2024VeyMontPermissions/0-TTT/0-TTT.pvl
@@ -1,5 +1,5 @@
 inline resource ticTacToeAnnotations(Player p1, Player p2) =
-  // p1.myMark == 0 ** p2.myMark == 1 **
+  p1.myMark == 0 ** p2.myMark == 1 **
   p1.turn != p2.turn **
   p1.equalBoard(p2);
 
@@ -8,7 +8,6 @@ choreography TTT() {
   endpoint p2 = Player(1, false);
 
   context (\chor ticTacToeAnnotations(p1, p2));
-  requires p1.myMark == 0 ** p2.myMark == 1;
   ensures (\chor p1.gameFinished() && p2.gameFinished());
   run {
     loop_invariant (\chor ticTacToeAnnotations(p1, p2));

diff --git a/src/main/vct/options/Options.scala b/src/main/vct/options/Options.scala
@@ -311,14 +311,17 @@ case object Options {
       ).children(
         opt[Unit]("choreography").abbr("chor").action((_, c) =>
           c.copy(veymontSkipImplementationVerification = true)
-        ),
+        ).text("Only perform verification of the choreography."),
         opt[Unit]("implementation").abbr("impl")
-          .action((_, c) => c.copy(veymontSkipChoreographyVerification = true)),
+          .action((_, c) => c.copy(veymontSkipChoreographyVerification = true))
+          .text("Only perform verification of the generated implementation."),
         opt[Unit]("generate").abbr("gen").action((_, c) =>
           c.copy(
             veymontSkipChoreographyVerification = true,
             veymontSkipImplementationVerification = true,
           )
+        ).text(
+          "Only generate an implementation, and skip the choreography and implementation verification steps"
         ),
         opt[Path]("veymont-output").valueName("<path>")
           .action((path, c) => c.copy(veymontOutput = Some(path))).text(

diff --git a/src/rewrite/vct/rewrite/veymont/generation/GenerateImplementation.scala b/src/rewrite/vct/rewrite/veymont/generation/GenerateImplementation.scala
@@ -4,6 +4,7 @@ import com.typesafe.scalalogging.LazyLogging
 import hre.util.ScopedStack
 import vct.col.ast.{
   And,
+  TVoid,
   ApplicableContract,
   Assert,
   Assign,
@@ -197,12 +198,14 @@ case class GenerateImplementation[Pre <: Generation]()
           )
 
           globalDeclarations.declare(
-            procedure(
+            new Procedure(
+              contract = chor.contract.rewriteDefault(),
+              returnType = TVoid[Post](),
               args = variables.dispatch(chor.params),
               body = Some(mainBody),
-              blame = PanicBlame("TODO: Procedure"),
-              contractBlame = PanicBlame("TODO: Procedure contract"),
-            )(chor.o)
+              outArgs = Seq(),
+              typeArgs = Seq(),
+            )(PanicBlame("TODO: Procedure"))(chor.o)
           )
         }
       case other => super.dispatch(other)

diff --git a/test/main/vct/test/integration/examples/veymont/TechnicalVeyMontSpec.scala b/test/main/vct/test/integration/examples/veymont/TechnicalVeyMontSpec.scala
@@ -3,6 +3,20 @@ package vct.test.integration.examples.veymont
 import vct.test.integration.helper.VeyMontSpec
 
 class TechnicalVeyMontSpec extends VeyMontSpec {
+  implementation(
+    desc = "Run contract can depend on choreography contract",
+    pvl = """
+  class Storage {}
+
+  requires x > 0;
+  choreography Chor(int x) {
+    endpoint alex = Storage();
+
+    requires x > 0;
+    run { }
+  }""",
+  )
+
   choreography(
     desc = "Bobby may receive permission for its target location",
     pvl = """

diff --git a/test/main/vct/test/integration/helper/VeyMontSpec.scala b/test/main/vct/test/integration/helper/VeyMontSpec.scala
@@ -99,8 +99,8 @@ class VeyMontSpec extends VercorsSpec with LazyLogging {
   def implementation(
       pvl: String = null,
       desc: String = null,
-      input: Path,
-      inputs: Seq[Path],
+      input: Path = null,
+      inputs: Seq[Path] = null,
       flags: Seq[String] = Seq(),
       flag: String = null,
       fail: String = null,