Контракты C # Code: Являются ли постусловия на членах доступными из других потоков бесполезными?

Question

после некоторого размышления я пришел к выводу, что постусловия в методах полезны только тогда, когда налагаются на возвращаемое значение, параметры ref и out , но не на поля, ни статические, ни на какие-либо пример. Причина в том, что при вызове этого метода статический анализ этого вызова не может ничего сделать с постусловиями в поле, потому что другие потоки уже могли изменить это поле на любое состояние и, следовательно, не обязательно соответствуют постусловию. Я делаю вывод, что постусловия, налагаемые на что-либо доступное более чем одним потоком, которые в основном являются только полями, бесполезны, и это оставляет только полезность постусловий для возвращаемых значений и out и ref параметры. Инвариант - это единственная форма постусловий для полей, которые не отрицаются с помощью потоков.

Я спрашиваю, является ли это рассуждение ошибочным и не хватает ли я аргументов для какой-либо немета-цели постусловий на полях. Под «мета» я подразумеваю все, что также может быть достигнуто другими средствами, в частности, комментируя.

Answer 1

статический анализ этого вызова не может сделать что-нибудь с постусловиями на поле

Он может убедиться, что вы удовлетворили их. Если другой поток изменяет значение поля так, что когда вы возвращаете постусловие, оно не сохраняется, то ваш класс используется небезопасным для потока способом в соответствии с его спецификацией безопасности потока (в противном случае средства синхронизации, которые он реализует для обеспечения безопасности потока предотвратил бы это в первую очередь). Здесь вы говорите: «Если вы используете класс так, как он не поддерживает, постусловия не помогают». Но это меньше всего беспокоит вас в этом случае.

Инвариант является единственной формой постусловия на полях не отменяются по ниткам.

Тот же аргумент, который вы использовали для постусловий, можно использовать для инвариантов классов: другие потоки могли начать модифицировать объект и оставить его в несовместимом состоянии (они могут делать это до тех пор, пока открытый метод, который его выполняет, не вернулся) , так что когда вы возвращаете, инвариант не сохраняется.