diff options
| author |  tabarbe <unknown> | 2010-07-30 18:12:25 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-07-30 18:12:25 +0000 |
| commit | b8a3c4ebd639c1481e543fcba2dae7829dac42e4 (patch) | |
| tree | 6f7121fad63a0381a7b539d1a632ea07e87948f6 /Util/Code Snippets/contractinvnonnullelem.snippet | |
| parent | b16618051e08f0b286e9f2171bdf6ed5efa552b1 (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/contractinvnonnullelem.snippet')
| -rw-r--r-- | Util/Code Snippets/contractinvnonnullelem.snippet | 31 |
1 files changed, 31 insertions, 0 deletions
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>
|