14. Що розуміється під коректністю програмного забезпечення?

Коректність ПЗ – відповідність програмних елементів з заданою специфікацією.

Формула коректності (тріада Хоара)

{P} A {Q}

Будь-яке виконання операції А, яке починається у стані, де ствердження Р є істинним, завершиться у стані, де буде істинним Q.

Р – передумова, встановлює властивості, які мають виконуватися кожен раз при виклику підпрограми.

Q – посту-умова, встановлює властивості, які гарантуються підпрограмою при її завершенні.

15. Як визначаються передумови у с# Code Contracts?

Передумови декларують умови, необхідні для роботи методу, виражаються за допомогоюContract.Requires () ізазвичай використовуються для перевірки вхідних параметрів.Функція Requires () приймає як параметр логічний вираз що виражає умовуконтракту. Так само існує перевантажена функція, що приймає в якості другогопараметра рядок - повідомлення, що використовується при порушенні умови.

16. Як визначаються постумови у с# Code Contracts?

Для їх вказівки в Code Contracts використовується метод Contract.Ensures ().

Тут розкривається ще одна відмінність Code Contracts від реалізації за допомогою блоку if-throw. Справа в тому, що виклики Contract.Ensures () не обов'язково розміщувати в кінці методу. Всі умови можна розташувати на його початку.

17. Які методи використовуються в посту мовах для перевірки значень, що повертаються, у с# Code Contracts.

void Ensures(bool condition) - Специфікує контракт постумови метода для вихідної умови condition

void Ensures (bool condition, string userMessage) - Специфікує контракт постумови метода для вихідної умови condition та виводить повідомлення userMessage, якщо умова контракту не виконується

void Ensures <TException>(bool condition)where TException : Exception - Специфікує контракт постумови condition метода та генерує виняткову ситуацію TException, якщо умова контракту не виконується

void Ensures <TException>(bool condition,string userMessage)where TException : Exception - Специфікує контракт постумови condition метода та генерує виняткову ситуацію TException з повідомленням userMessage, якщо умова контракту не виконується

18. Як визначаються інваріанти об’єктів у с# Code Contracts.

Інваріант класу – це ствердження, яке виражає загальні узгоджені обмеження, що справедливі на всьому протязі обчислень і застосовуються до кожного екземпляру класу як цілому. Інваріанти класу формулюються в термінах атрибутів класів і застосовуються до всіх об’єктів цього класу.

public static void Invariant(bool condition) - Специфікує інваріантний контракт

void Invariant(bool condition, string userMessage) - Специфікує інваріантний контракт та виводить повідомлення userMessage, якщо умова контракту не виконується

19. Які символи та правила можуть використовуватися в узгодженнях щодо вибору

позначень типів та об’єктів?

Можуть у назві використовуватися:

• Прописні букви

  • На початку кожного слова

  • На початку кожного слова, окрім першого

  • Усі прописні

• Знаки підкреслення – розподіл слів у ідентифікаторі (UNIX, рекомендація стандарту GNU)

• Ініціали

• Префікси

Рекомендації Microsoft програмістам C#

Не використовувати венгерську нотацію і у позначеннях об’єктів і типів знаків підкреслення, дефісів і інших не алфавітно-цифрових символів.