Skip to content
This repository was archived by the owner on Jul 15, 2023. It is now read-only.

Merge pull request 84 #103

Merged
SergeyTeplyakov merged 8 commits into from
Jul 9, 2015
Merged

Merge pull request 84 #103

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
164de22
Fix various system contracts
tom-englert Jul 3, 2015
87830ee
Improve comment
tom-englert Jul 3, 2015
96bcb71
Restore some contract changes that have been moved to another branch
tom-englert Jul 3, 2015
24b0cdd
Add missing contract for Collection
tom-englert Jul 3, 2015
f22ab89
Restore: Contracts that the checker can't proof.
tom-englert Jul 3, 2015
0f7910e
Fix contracts of ObservableCollection
tom-englert Jul 3, 2015
400467b
Fix wrong contract due to wrong method documentation
tom-englert Jul 4, 2015
48d2476
Merge pull request #84 from tom-englert/ContractFixes
sharwell Jul 9, 2015
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -328,8 +328,11 @@
<Compile Include="System.Collections.Concurrent.ConcurrentDictionary.cs" />
<Compile Include="System.Collections.Generic.IReadOnlyCollection.cs" />
<Compile Include="System.Collections.Generic.IReadOnlyList.cs" />
<Compile Include="System.Collections.ObjectModel.Collection.cs" />
<Compile Include="System.Diagnostic.Tracing.EventSource.cs" />
<Compile Include="System.Diagnostic.Tracing.EventWrittenEventArgs.cs" />
<Compile Include="System.Globalization.CalendarWeekRule.cs" />
<Compile Include="System.Globalization.DateTimeFormatInfo.cs" />
<Compile Include="System.IO.DirectoryNotFoundException.cs" />
<Compile Include="System.IO.FileNotFoundException.cs" />
<Compile Include="System.IO.PathTooLongException.cs" />
Expand Down Expand Up @@ -848,6 +851,7 @@ Include="System.Security.Principal.WindowsPrincipal.cs" /> -->
<Compile Include="System.Security.Cryptography.HashAlgorithm.cs" />
<Compile Include="System.Security.Cryptography.ICryptoTransform.cs" />
<Compile Include="System.Security.Cryptography.MD5.cs" />
<Compile Include="System.Security.Cryptography.SymmetricAlgorithm.cs" />
<Compile Include="System.Security.Principal.IIdentity.cs" />
<Compile Include="System.Security.Principal.IPrincipal.cs" />
<Compile Include="System.Security.Principal.SecurityIdentifier.cs" />
Expand Down
16 changes: 10 additions & 6 deletions Microsoft.Research/Contracts/MsCorlib/System.Collections.Generic.IDictionary.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,11 +167,13 @@ TValue IDictionary<TKey, TValue>.this[TKey key]
{
get
{
Contract.Requires(!ReferenceEquals(key, null));
// Contract.Requires(ContainsKey(key));
throw new NotImplementedException();
}
set
{
Contract.Requires(!ReferenceEquals(key, null));
// Contract.Ensures(ContainsKey(key));
//Contract.Ensures(old(ContainsKey(key)) ==> Count == old(Count));
//Contract.Ensures(!old(ContainsKey(key)) ==> Count == old(Count) + 1);
Expand All @@ -181,37 +183,39 @@ TValue IDictionary<TKey, TValue>.this[TKey key]

void IDictionary<TKey, TValue>.Add(TKey key, TValue value)
{
Contract.Requires(!ReferenceEquals(key, null));
// Contract.Requires(!ContainsKey(key));
//modifies this.*;
//Contract.Ensures(ContainsKey(key));
}

bool IDictionary<TKey, TValue>.ContainsKey(TKey key)
public bool ContainsKey(TKey key)
{
var @this = (IDictionary<TKey, TValue>)this;
Contract.Ensures(!Contract.Result<bool>() || @this.Count > 0);
Contract.Requires(!ReferenceEquals(key, null));
Contract.Ensures(!Contract.Result<bool>() || (Count > 0));

throw new NotImplementedException();
}

bool IDictionary<TKey, TValue>.Remove(TKey key)
{
Contract.Requires(!ReferenceEquals(key, null));
// Contract.Ensures(!Contract.Result<bool>() || Contract.OldValue(ContainsKey(key)) && !ContainsKey(key));
throw new NotImplementedException();
}

bool IDictionary<TKey, TValue>.TryGetValue(TKey key, out TValue value)
{
var @this = (IDictionary<TKey, TValue>)this;
Contract.Ensures(Contract.Result<bool>() == @this.ContainsKey(key));
Contract.Requires(!ReferenceEquals(key, null));
Contract.Ensures(Contract.Result<bool>() == ContainsKey(key));
throw new NotImplementedException();
}

#endregion

#region ICollection<KeyValuePair<TKey,TValue>> Members

int ICollection<KeyValuePair<TKey, TValue>>.Count
public int Count
{
get { throw new NotImplementedException(); }
}
Expand Down
Loading