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 | |
| 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')
| -rw-r--r-- | Util/Code Snippets/contractassertnonnull.snippet | 31 | ||||
| -rw-r--r-- | Util/Code Snippets/contractassertnonnullelem.snippet | 31 | ||||
| -rw-r--r-- | Util/Code Snippets/contractensuresnonnullelem.snippet | 31 | ||||
| -rw-r--r-- | Util/Code Snippets/contractensuresvalret.snippet | 31 | ||||
| -rw-r--r-- | Util/Code Snippets/contractinvnonnullelem.snippet | 31 | ||||
| -rw-r--r-- | Util/Code Snippets/contractrequiresnonnullelem.snippet | 31 |
6 files changed, 186 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>
diff --git a/Util/Code Snippets/contractassertnonnullelem.snippet b/Util/Code Snippets/contractassertnonnullelem.snippet new file mode 100644 index 00000000..86273d71 --- /dev/null +++ b/Util/Code Snippets/contractassertnonnullelem.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(cce.NonNullElements(...))</Title>
+ <Shortcut>cann</Shortcut>
+ <Description>Emits a 'Contract.Assert' 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.Assert(cce.NonNullElements($collection$));$end$]]></Code>
+ </Snippet>
+ </CodeSnippet>
+</CodeSnippets>
diff --git a/Util/Code Snippets/contractensuresnonnullelem.snippet b/Util/Code Snippets/contractensuresnonnullelem.snippet new file mode 100644 index 00000000..fabd9d1a --- /dev/null +++ b/Util/Code Snippets/contractensuresnonnullelem.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.Ensures(cce.NonNullElements(Contract.Result<...>()))</Title>
+ <Shortcut>cenn</Shortcut>
+ <Description>Emits a 'Contract.Ensures' 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>List<string></Default>
+ <Function>
+ </Function>
+ </Object>
+ </Declarations>
+ <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Ensures(cce.NonNullElements(Contract.Result<$collection$>()));$end$]]></Code>
+ </Snippet>
+ </CodeSnippet>
+</CodeSnippets>
\ No newline at end of file diff --git a/Util/Code Snippets/contractensuresvalret.snippet b/Util/Code Snippets/contractensuresvalret.snippet new file mode 100644 index 00000000..c1e5ef56 --- /dev/null +++ b/Util/Code Snippets/contractensuresvalret.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.Ensures(Contract.ValueAtReturn(...)!=null)</Title>
+ <Shortcut>cern</Shortcut>
+ <Description>Emits a 'Contract.Ensures' non-null out or ref parameter clause</Description>
+ <Author>tabarbe</Author>
+ </Header>
+ <Snippet>
+ <Imports>
+ <Import>
+ <Namespace>System.Diagnostics.Contracts</Namespace>
+ </Import>
+ </Imports>
+ <Declarations>
+ <Object Editable="true">
+ <ID>value</ID>
+ <ToolTip>Value that must not be null</ToolTip>
+ <Default>arg</Default>
+ <Function>
+ </Function>
+ </Object>
+ </Declarations>
+ <Code Language="CSharp" Kind="method body"><![CDATA[Contract.Ensures(Contract.ValueAtReturn($value$)!=null);$end$]]></Code>
+ </Snippet>
+ </CodeSnippet>
+</CodeSnippets>
\ No newline at end of file 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>
diff --git a/Util/Code Snippets/contractrequiresnonnullelem.snippet b/Util/Code Snippets/contractrequiresnonnullelem.snippet new file mode 100644 index 00000000..eb07bc66 --- /dev/null +++ b/Util/Code Snippets/contractrequiresnonnullelem.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.Requires(cce.NonNullElements(...))</Title>
+ <Shortcut>crnn</Shortcut>
+ <Description>Emits a 'Contract.Requires' 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.Requires(cce.NonNullElements($collection$));$end$]]></Code>
+ </Snippet>
+ </CodeSnippet>
+</CodeSnippets>
|