feat(TestModels): Resource

TestModels/.gitignore

@@ -0,0 +1,17 @@
+# .NET Test Results
+**/TestResults
+
+# Dafny Generated .NET
+**/ImplementationFromDafny.cs
+**/TestsFromDafny.cs
+
+# .NET Artifacts
+**/bin
+**/obj
+
+# JetBrains
+**/.idea/
+
+# Generated Dafny
+**/*Types.dfy
+**/*TypesWrapped.dfy

TestModels/resources/Makefile

@@ -0,0 +1,23 @@
+# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+CORES=2
+PWD := $(dir $(realpath $(lastword $(MAKEFILE_LIST))))
+
+polymorph_dafny:
+	gradle -p ../../smithy-polymorph run --args="\
+	  --output-dafny \
+      --include-dafny $(PWD)/../dafny-dependencies/StandardLibrary/src/Index.dfy \
+      --model $(PWD)/Model \
+      --dependent-model $(PWD)/../dafny-dependencies/Model \
+      --namespace simple.resources";
+	gradle -p ../../smithy-polymorph run --args="\
+	  --output-dafny \
+	  --output-local-service-test $(PWD)/Model \
+      --include-dafny $(PWD)/../dafny-dependencies/StandardLibrary/src/Index.dfy \
+      --model $(PWD)/Model \
+      --dependent-model $(PWD)/../dafny-dependencies/Model \
+      --namespace simple.resources";
+
+clean:
+	rm $(PWD)/Model/*.dfy

TestModels/resources/Model/resources.smithy

@@ -0,0 +1,81 @@
+namespace simple.resources
+
+@aws.polymorph#localService(
+  sdkId: "SimpleResources",
+  config: SimpleResourcesConfig,
+)
+service SimpleResources {
+  version: "2021-11-01",
+  resources: [],
+  operations: [ GetResources ],
+  errors: [ SimpleResourceException ],
+}
+
+structure SimpleResourcesConfig {}
+
+// This operation MUST
+// return the values given in the Resources.
+// The internal config MUST somehow differ,
+// and this additional information MUST be returned.
+operation GetResources {
+  input: GetResourcesInput,
+  output: GetResourcesOutput,
+}
+
+structure GetResourcesInput {
+  value: String
+}
+
+structure GetResourcesOutput {
+  @required
+  output: SimpleResourceReference
+}
+
+@aws.polymorph#reference(resource: SimpleResource)
+structure SimpleResourceReference {}
+
+resource SimpleResource {
+  operations: [ GetResourceData ]
+}
+
+operation GetResourceData {
+  input: GetResourceDataInput,
+  output: GetResourceDataOutput,
+}
+
+structure GetResourceDataInput {
+  blobValue: Blob,
+  booleanValue: Boolean,
+  stringValue: String,
+//  byteValue: Byte,
+//  shortValue: Short,
+  integerValue: Integer,
+  longValue: Long,
+//  floatValue: Float,
+//  doubleValue: Double,
+//  bigIntegerValue: BigInteger,
+//  bigDecimalValue: BigDecimal,
+//  timestampValue: Timestamp,
+}
+
+structure GetResourceDataOutput {
+  blobValue: Blob,
+  booleanValue: Boolean,
+  stringValue: String,
+//  byteValue: Byte,
+//  shortValue: Short,
+  integerValue: Integer,
+  longValue: Long,
+//  floatValue: Float,
+//  doubleValue: Double,
+//  bigIntegerValue: BigInteger,
+//  bigDecimalValue: BigDecimal,
+//  timestampValue: Timestamp,
+}
+
+@error("client")
+structure SimpleResourceException {
+  @required
+  message: String,
+}
+

TestModels/resources/src/Config.dfy

@@ -0,0 +1,23 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../Model/SimpleResourcesTypes.dfy"
+
+module Config {
+  import opened StandardLibrary
+  import Types = SimpleResourcesTypes    
+
+  datatype Config = Config(
+    nameonly name: string,
+    nameonly modified: bool := false
+  )
+
+  predicate method ValidInternalConfig?(config: Config)
+  {
+    && |config.name| > 0
+  }
+
+  function ModifiesInternalConfig(config: Config): set<object>
+  {{}}
+
+}

TestModels/resources/src/SimpleResource.dfy

@@ -0,0 +1,75 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../Model/SimpleResourcesTypes.dfy"
+include "./Config.dfy"
+
+module SimpleResource {
+  import opened StandardLibrary
+  import opened Wrappers
+  import opened Config    
+  import Types = SimpleResourcesTypes    
+
+  class SimpleResource extends Types.ISimpleResource
+  {
+    const config: Config
+
+    predicate ValidState()
+      ensures ValidState() ==> History in Modifies
+    {
+      && History in Modifies
+      && ModifiesInternalConfig(config) <= Modifies
+      && History !in ModifiesInternalConfig(config)
+      && ValidInternalConfig?(config)
+    }
+
+    const value: string
+
+    constructor (
+      value: string,
+      config: Config
+    )
+      requires ValidInternalConfig?(config)
+      ensures this.value == value
+      ensures this.config == config
+      ensures ValidState() && fresh(History) && fresh(Modifies - ModifiesInternalConfig(config))
+    {
+      this.value := value;
+      this.config := config;
+
+      History := new Types.ISimpleResourceCallHistory();
+      Modifies := { History } + ModifiesInternalConfig(config);
+    }
+
+    predicate GetResourceDataEnsuresPublicly(
+      input: Types.GetResourceDataInput,
+      output: Result<Types.GetResourceDataOutput, Types.Error>
+    ) {true}
+
+    method GetResourceData'(
+      input: Types.GetResourceDataInput
+    ) returns (
+      output: Result<Types.GetResourceDataOutput, Types.Error>
+    )
+      requires ValidState()
+      modifies Modifies - {History}
+      decreases Modifies - {History}
+      ensures && ValidState()
+      ensures GetResourceDataEnsuresPublicly(input, output)
+      ensures unchanged(History)
+    {
+      var rtnString: string := if input.stringValue.Some? then
+        this.config.name + " " + input.stringValue.value
+      else
+        this.config.name;
+      var rtn: Types.GetResourceDataOutput := Types.GetResourceDataOutput(
+        blobValue := input.blobValue,
+        booleanValue := input.booleanValue,
+        stringValue := Option.Some(rtnString),
+        integerValue := input.integerValue,
+        longValue := input.longValue
+      );
+      return Success(rtn);  
+    }
+  }
+}

TestModels/resources/src/SimpleResourcesOperations.dfy

@@ -0,0 +1,44 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../Model/SimpleResourcesTypes.dfy"
+include "./Config.dfy"
+include "./SimpleResource.dfy"
+
+module SimpleResourcesOperations refines AbstractSimpleResourcesOperations {
+  import Config
+  import SimpleResource
+
+  type InternalConfig = Config.Config
+
+  predicate GetResourcesEnsuresPublicly(
+    input: GetResourcesInput,
+    output: Result<GetResourcesOutput, Error>
+  ) {true}
+
+  method GetResources(
+    config: InternalConfig,
+    input: GetResourcesInput
+  ) returns (
+    output: Result<GetResourcesOutput, Error>
+  )
+  {
+    :- Need(Config.ValidInternalConfig?(config),
+      Types.SimpleResourceException(
+      message := "Simple Resource Client has become invalid")
+    );
+    :- Need(input.value.Some?,
+      Types.SimpleResourceException(
+      message := "Input Value MUST be set")
+    );
+    var resource := new SimpleResource.SimpleResource(
+      input.value.value,
+      config
+     );
+     var result: GetResourcesOutput := GetResourcesOutput(
+      output := resource
+    );
+    return Success(result);  
+  }
+
+}