{"action":"created","issue":{"url":"https://api.github.com/repos/Microsoft/CodeContracts/issues/265","labels_url":"https://api.github.com/repos/Microsoft/CodeContracts/issues/265/labels{/name}","comments_url":"https://api.github.com/repos/Microsoft/CodeContracts/issues/265/comments","events_url":"https://api.github.com/repos/Microsoft/CodeContracts/issues/265/events","html_url":"https://github.com/Microsoft/CodeContracts/issues/265","id":111324102,"number":265,"title":"Ensures in override not proven","user":{"login":"Nathan-022","id":2570246,"avatar_url":"https://avatars.githubusercontent.com/u/2570246?v=3","gravatar_id":"","url":"https://api.github.com/users/Nathan-022","html_url":"https://github.com/Nathan-022","followers_url":"https://api.github.com/users/Nathan-022/followers","following_url":"https://api.github.com/users/Nathan-022/following{/other_user}","gists_url":"https://api.github.com/users/Nathan-022/gists{/gist_id}","starred_url":"https://api.github.com/users/Nathan-022/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Nathan-022/subscriptions","organizations_url":"https://api.github.com/users/Nathan-022/orgs","repos_url":"https://api.github.com/users/Nathan-022/repos","events_url":"https://api.github.com/users/Nathan-022/events{/privacy}","received_events_url":"https://api.github.com/users/Nathan-022/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-10-14T05:01:24Z","updated_at":"2015-10-14T16:57:34Z","closed_at":null,"body":"I have overridden TypeConverter.ConvertFrom and attempted to Ensure the return value is not null. The base TypeConverter class doesn't ensure this, so I am making the postcondition stronger in my custom implementation.\r\n\r\nFrom my understanding, inheritance works like:\r\n* If a subclass overrides the behavior of a method of a base class (or implements and interface), the preconditions it specifies can only be equivalent to or weaker than the base class\r\n* If a subclass overrides the behavior of a method of a base class (or implements and interface), the postconditions it specifies can only be equivalent to or stronger than the base class.\r\n\r\nFrom this description, I should be able to have a stronger postcondition in the subclass (non null return) and have it respected by the analysis tool, however in practice this isn't working.\r\n\r\nIs my interpretation incorrect or is this a bug in the static analysis?\r\n\r\nSample code:\r\n\r\n```csharp\r\nCustomTypeConverter converter = new CustomTypeConverter();\r\nobject converted = converter.ConvertFrom(null, CultureInfo.CurrentCulture, value);\r\nContract.Assume(converted != null, \"Contracts analysis doesn't realise that the non null return was ensured, the below code gives an 'unboxing null reference' warning\");\r\nthis = (CustomType)converted;\r\n```\r\n\r\nInside the typeconverter, something like:\r\n\r\n```csharp\r\npublic override object ConvertFrom(ITypeDescriptorContext context, System.Globalization.CultureInfo culture, object value)\r\n{\r\n\tContract.Ensures(Contract.Result<object>() != null);\r\n\treturn \"example\";\r\n}\r\n```"},"comment":{"url":"https://api.github.com/repos/Microsoft/CodeContracts/issues/comments/148115902","html_url":"https://github.com/Microsoft/CodeContracts/issues/265#issuecomment-148115902","issue_url":"https://api.github.com/repos/Microsoft/CodeContracts/issues/265","id":148115902,"user":{"login":"mike-barnett","id":5694676,"avatar_url":"https://avatars.githubusercontent.com/u/5694676?v=3","gravatar_id":"","url":"https://api.github.com/users/mike-barnett","html_url":"https://github.com/mike-barnett","followers_url":"https://api.github.com/users/mike-barnett/followers","following_url":"https://api.github.com/users/mike-barnett/following{/other_user}","gists_url":"https://api.github.com/users/mike-barnett/gists{/gist_id}","starred_url":"https://api.github.com/users/mike-barnett/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mike-barnett/subscriptions","organizations_url":"https://api.github.com/users/mike-barnett/orgs","repos_url":"https://api.github.com/users/mike-barnett/repos","events_url":"https://api.github.com/users/mike-barnett/events{/privacy}","received_events_url":"https://api.github.com/users/mike-barnett/received_events","type":"User","site_admin":false},"created_at":"2015-10-14T16:57:34Z","updated_at":"2015-10-14T16:57:34Z","body":"You are correct in the theory of modifying contracts. Note that just as an implementation decision, Code Contracts does not allow you to weaken preconditions, but only to strengthen postconditions.\r\n\r\nIt looks to me as if that is a bug in the static checker. However, now that Francesco is not working on the project any longer, it isn't clear if there is anyone who will be able to fix it."}}