Партнерка на США и Канаду по недвижимости, выплаты в крипто

  • 30% recurring commission
  • Выплаты в USDT
  • Вывод каждую неделю
  • Комиссия до 5 лет за каждого referral

Установка VCC

Необходимое программное обеспечение:

    .Net v4.0 or later F# 2.0 Redistributable F# Power Pack Microsoft Visual C++ 2010 Redistributable Package Visual Studio 2010 or 2012 - Express-версии не поддерживаются.

После установки обязательного ПО переходим к установке непосредственно VCC. Скачиваем инсталлятор с CodePlex по адресу:

http://vcc. /releases/view/101889

Устанавливаем, следуя инструкциям на экране. Далее нужно добавить функционал VCC к возможностям Visual Studio. Для этого:


Нужно запустить Visual Studio и создать пустой C++ проект. View->Other Windows->Property Manager. Эта последовательность действий открывает менеджер настроек проектов. Работа с Property Manager'ом:
    Если вы хотите добавить поддержку VCC только для одного проекта, двойным нажатием по его имени откройте настройки. Если вы хотите добавить поддержку VCC для всех проектов раскройте дерево для вашего проекта и откройте двойным нажатием файл Microsoft. Cpp. Win32.User.

В настройках, нажмите на "VC++ Directories", далее на "Include Directories", затем на стрелочку справой стороны списка директорий и нажмите "edit".

Создайте новую директорию нажатием на изображение папки . Далее откройте навигатор, нажатием на и перейдите к папке

/Program Files (x86)/Microsoft Research/Vcc/Headers/

(The (x86) присутствует в пути, только на 64-bit версии Windows.)

После выполнения описанных операций необходимо проверить, что функционал VCC интегрирован в Visual Studio.

Создайте в проекте новый файл, например "test. c". Добавьте следующий код:

Правым кликом на "test()" откройте контекстное меню, в нём должны появиться новые пункты для верификации.

Выберите Verify File: 'test. c' и через несколько секунд в консоли должно появиться сообщение

Аннотации в VCC

       Перед запуском VCC исходный код нужно аннотировать, для того чтобы сообщить верификатору, что делает код и задать какие-либо условия работоспособности кода.        Аннотации обозначаются как "_(...)", внутри скобок записываются специальные теги и условия по которым они должны работать.

assert - утверждение, запись _(assert X), означает, что мы просим VCC доказать утверждение X.

Пример:

Рассмотрим простую программу, вычисляющую минимум x и y. Аннотация  _(assert z <= x) говорит о том, что в конце выполнения программы переменная  z будет не больше чем х. Если изменить знак <= внутри аннотации например на >, то верификатор вернёт сообщение об ошибке.

assume - от слова assumption (предположение), запись _(assume X), означает, что мы предполагаем, что утверждение X истинно, если это не так - оставшаяся часть кода игнорируется.

Пример:

При верификации данной части кода, VCC не выдаст никаких ошибок, т. к. если х=0, то строка y = 100/x игнорируется. Если же убрать аннотацию, то сразу получим сообщение об ошибке.

requires - предусловие - проверка условия на входе в функцию.

ensures - постусловие - проверка условия на выходе из функции.

Аннотации _(requires X) и _(ensures X ) записываются после имени функции, например так:

В данном случае перед выполнением функции 'min' переменная 'a' должна быть больше и по завершению выполнения должно выполняться условие 

((result <= a) && (result <= b))