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 | |
| 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')
| -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 | ||||
| -rw-r--r-- | Util/Return of Multilingual Greetings.txt | 9 |
7 files changed, 186 insertions, 9 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>
diff --git a/Util/Return of Multilingual Greetings.txt b/Util/Return of Multilingual Greetings.txt deleted file mode 100644 index 8adbe9ea..00000000 --- a/Util/Return of Multilingual Greetings.txt +++ /dev/null @@ -1,9 +0,0 @@ -Hello
-Hola
-Adios
-Goodbye
-Auf viderzen (how should that be spelled?)
-Aloha
-Hasta la vista
-Arrivederci
-See ya later
\ No newline at end of file |