Boogie/Dafny: Boogie and Dafny's conversion to C# and Code Contracts does not need to mean that adding functionality will take longer than it had before, now that the handy Spec# non-null typesystem and verification keywords no longer are used. Here are some handy Code Snippets which can be implemented in Visual Studio in order to make adding to the Boogie codebase rapid.

1 files changed, 31 insertions, 0 deletions

diff --git a/Util/Code Snippets/contractassertnonnull.snippet b/Util/Code Snippets/contractassertnonnull.snippet
new file mode 100644
index 00000000..4979600a
--- /dev/null
+++ b/Util/Code Snippets/contractassertnonnull.snippet
@@ -0,0 +1,31 @@
+<?xml version="1.0" encoding="utf-8"?>

+<CodeSnippets xmlns="http://schemas.microsoft.com/VisualStudio/2005/CodeSnippet">

+  <CodeSnippet Format="1.0.0">

+    <Header>

+      <SnippetTypes>

+        <SnippetType>Expansion</SnippetType>

+      </SnippetTypes>

+      <Title>Contract.Assert(...!=null)</Title>

+      <Shortcut>can</Shortcut>

+      <Description>Emits a 'Contract.Assert' non-null clause</Description>

+      <Author>tabarbe</Author>

+    </Header>

+    <Snippet>

+      <Imports>

+        <Import>

+          <Namespace>System.Diagnostics.Contracts</Namespace>

+        </Import>

+      </Imports>

+      <Declarations>

+        <Object Editable="true">

+          <ID>condition</ID>

+          <ToolTip>condition that must not be null</ToolTip>

+          <Default>arg</Default>

+          <Function>

+          </Function>

+        </Object>

+      </Declarations>

+      <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Assert($condition$ != null);$end$]]></Code>

+    </Snippet>

+  </CodeSnippet>

+</CodeSnippets>