Code Contracts – inaccuracies (visibility, subtype)
- Dominant language
- No language data
- Stars
- 4.8k
- Forks
- 6.1k
- Avg merge
- 15h 21m
- Merged PRs (30d)
- 370
Description
From [Exceptional Postconditions](https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts#exceptional-postconditions)
> `Contract.EnsuresOnThrow(this.F > 0);`
> The argument is the condition that must be `true` whenever an exception that is a subtype of `T` is thrown.
From [Contract.EnsuresOnThrow Method](https://docs.microsoft.com/en-us/dotnet/api/system.diagnostics.contracts.contract.ensuresonthrow?view=net-5.0)
> `[System.Diagnostics.Conditional("CONTRACTS_FULL")] `
> `public static void EnsuresOnThrow (bool condition) where TException : Exception;`
> The `condition` parameter specifies a postcondition that is expected to be `true` when the enclosing method or property terminates abnormally and an exception of type `TException` is thrown.
It is type of `T` not subtype of `T`. AFAIK subtype is of type of its base type.
---
From [Postconditions](https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts#postconditions)
> Unlike preconditions, postconditions may reference members with less visibility. A client may not be able to understand or make use of some of the information expressed by a postcondition using private state, but this does not affect the client's ability to use the method correctly.
From [Visibility](https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts#visibility)
> All members mentioned in a contract must be at least as visible as the method in which they appear. For example, a private field cannot be mentioned in a precondition for a public method; clients cannot validate such a contract before they call the method.
It is fine that details are more specified in specific section (_Postconditions_) but _Visibility_ section appears as if provides exhausting list of behaviors (which it does not).
---
#### Document Details
⚠ *Do not edit this section. It is required for docs.microsoft.com ➟ GitHub issue linking.*
* ID: d92c6e0f-2503-fe90-2b96-3b0c2054e8dc
* Version Independent ID: 5612b486-e780-7625-12fb-f5478f1be7de
* Content: [Code Contracts](https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts)
* Content Source: [docs/framework/debug-trace-profile/code-contracts.md](https://github.com/dotnet/docs/blob/main/docs/framework/debug-trace-profile/code-contracts.md)
* Product: **dotnet-framework**
* GitHub Login: @gewarren
* Microsoft Alias: **dotnetcontent**
Contributor guide
Assessment
This issue has not been assessed yet.