summaryrefslogtreecommitdiff
path: root/Util/Code Snippets/contractassertnonnull.snippet
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-07-30 18:12:25 +0000
committerGravatar tabarbe <unknown>2010-07-30 18:12:25 +0000
commitb8a3c4ebd639c1481e543fcba2dae7829dac42e4 (patch)
tree6f7121fad63a0381a7b539d1a632ea07e87948f6 /Util/Code Snippets/contractassertnonnull.snippet
parentb16618051e08f0b286e9f2171bdf6ed5efa552b1 (diff)
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.
Diffstat (limited to 'Util/Code Snippets/contractassertnonnull.snippet')
-rw-r--r--Util/Code Snippets/contractassertnonnull.snippet31
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>