1. Напишите модель программы и модель требований, докажите полную корректность. Программа получает на вход указатель на массив из целых чисел и размер массива. Программа создает массив в два раза длиннее исходного, заполняет его значениями исходного массива (сначала один раз целиком, затем еще раз целиком) и возвращает указатель на начало этого массива.

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

  3. Напишите реализацию функции memcpy. По ней напишите модель программы, строго следуя тексту реализации. Напишите модель требований для этой функции. Докажите полную корректность модели программы относительно модели требований.

  4. Напишите реализацию функции memmove. По ней напишите модель программы, строго следуя тексту реализации. Напишите модель требований для этой функции. Докажите полную корректность модели программы относительно модели требований.