NyaOJ

题目描述

采用霍尔逻辑对一个内存分配程序的功能正确性进行形式化验证。

所有的空闲内存块保存在首指针为 free_list 的单向链表中，链表的每个元素包括 3 个字段：

saddr：该空闲内存块的首地址
block_size：该空闲内存块的大小
next：指向单向链表中的下一个空闲内存块的指针

内存分配函数 mem_alloc 包括两个参数：

指针类型 free_list
内存分配请求的块大小 size

内存分配算法是从 free_list 链表中从头开始，搜索空闲内存块大小至少为 size 的块，若存在，则将该块的指针返回，否则返回 NULL。

C 代码示例

struct block {
    void *saddr;
    int block_size;
    struct block *next;
};

struct block *mem_alloc(struct block *free_list, int size) {
    if (free_list == NULL) {
        return NULL;
    } else {
        if (free_list->block_size >= size) {
            struct block *res = free_list;
            free_list = free_list->next;
            return res;
        } else {
            struct block *q = free_list, *p = free_list->next;
            while (p != NULL && p->block_size < size) {
                q = p;
                p = p->next;
            }
            if (p != NULL) {
                q->next = p->next;
                return p;
            } else {
                return NULL;
            }
        }
    }
}

Lean4 证明

本题通过 Loom 程序验证框架进行。Loom 是一个通用框架，其中提供了类似 Dafny 的命令式程序验证工具示例 Velvet。

任务

(150 分) 证明 mem_alloc 函数符合由前、后条件给出的程序性质：

prove_correct mem_alloc by
  sorry

分值

mem_alloc 正确性证明: 150 分

总计: 150 分