From b8a3c4ebd639c1481e543fcba2dae7829dac42e4 Mon Sep 17 00:00:00 2001
From: tabarbe <unknown>
Date: Fri, 30 Jul 2010 18:12:25 +0000
Subject: 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.

---
 Util/Code Snippets/contractinvnonnullelem.snippet | 31 +++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 Util/Code Snippets/contractinvnonnullelem.snippet

(limited to 'Util/Code Snippets/contractinvnonnullelem.snippet')

diff --git a/Util/Code Snippets/contractinvnonnullelem.snippet b/Util/Code Snippets/contractinvnonnullelem.snippet
new file mode 100644
index 00000000..cd0ff1c6
--- /dev/null
+++ b/Util/Code Snippets/contractinvnonnullelem.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.Invariant(cce.NonNullElements(...))</Title>
+      <Shortcut>cinn</Shortcut>
+      <Description>Emits a 'Contract.Invariant' non-null elements clause</Description>
+      <Author>tabarbe</Author>
+    </Header>
+    <Snippet>
+      <Imports>
+        <Import>
+          <Namespace>System.Diagnostics.Contracts</Namespace>
+        </Import>
+      </Imports>
+      <Declarations>
+        <Object Editable="true">
+          <ID>collection</ID>
+          <ToolTip>collection whose elements must not be null</ToolTip>
+          <Default>arg</Default>
+          <Function>
+          </Function>
+        </Object>
+      </Declarations>
+      <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Invariant(cce.NonNullElements($collection$));$end$]]></Code>
+    </Snippet>
+  </CodeSnippet>
+</CodeSnippets>
-- 
cgit v1.2.3