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

Fix various system contracts #84

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

Fix various system contracts #84

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 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
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)
Copy link
Contributor

@sharwell sharwell Jul 3, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💭 I find the inconsistency between explicitly and implicitly implemented methods a bit confusing. Note that in addition to understanding why you made the change, I don't have a preference¹ towards implicit or explicit implementations of contract methods overall (each has their merits, and both work).

¹ I do have a preference, as noted in my comments on the contracts for Collection<T>.

Copy link
Contributor Author

@tom-englert tom-englert Jul 3, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For a ContractClass it's a bit different, it's clear that all methods are interface implementations. Here I changed to implicit methods because it removed unnecessary complexity from some of the contracts.

{
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