runtimeverificationinc/kframework-k Docker 镜像 - 轩辕镜像

K Framework Docker镜像文档

概述

本镜像为K Framework提供容器化部署方案。K Framework是一个开源的形式化方法工具包，支持编程语言的语法定义、语义规范及程序行为的形式化分析与验证。该Docker镜像预安装了完整的K工具链，旨在消除本地环境配置复杂性，确保跨平台一致性，方便开发者快速上手K Framework的各项功能。

核心功能与特性

• 完整工具链：包含K语言编译器（kore）、语法解析器（kast）、证明器（kprove）等核心工具
• 环境隔离：容器化运行避免系统依赖冲突，简化多版本K Framework并存管理
• 跨平台支持：兼容Linux、macOS及Windows（通过Docker Desktop）
• 版本一致性：通过镜像标签严格对应K Framework版本，确保开发与部署环境一致
• 轻量设计：基于精简基础镜像，优化镜像体积，减少资源占用

使用场景

• 编程语言设计：定义新编程语言的语法和操作语义
• 形式化验证：对程序性质（如安全性、正确性）进行数学化证明
• 语义研究：学术研究中快速验证语义定义的正确性
• 教育场景：教学环境中统一K Framework工具配置，降低入门门槛

使用方法

基本使用

拉取镜像

从Docker Hub拉取最新版本镜像：

bash
docker pull kframework/k:latest

指定版本（推荐生产环境使用具体版本号）：

bash
docker pull kframework/k:5.6.0  # 示例版本号，需替换为实际存在的标签

运行容器

以交互模式启动容器并进入shell：

bash
docker run -it --rm kframework/k:latest bash

挂载本地项目

通过 -v 参数挂载本地工作目录，实现容器内访问本地文件：

bash
# 将当前目录挂载到容器内的/workspace目录
docker run -it --rm -v $(pwd):/workspace -w /workspace kframework/k:latest bash

在容器内即可使用K工具处理本地文件，例如解析K定义文件：

bash
kast my_language.k --output kore  # 将K定义文件转换为KORE中间表示

直接执行命令

无需进入容器，直接在宿主机器执行K工具命令：

bash
# 验证程序性质
docker run -it --rm -v $(pwd):/workspace -w /workspace kframework/k:latest kprove spec.k

镜像标签说明

• latest：指向最新稳定版本
• X.Y.Z：特定版本标签（如5.6.0），对应K Framework的GitHub发布版本
• dev：开发分支快照，包含最新未发布功能（不稳定，仅供测试）

注意事项

• 本地文件操作需确保挂载目录权限正确，避免容器内文件读写失败
• 复杂项目建议使用docker-compose管理容器配置，例如持久化工具缓存
• 如需自定义工具链配置，可基于本镜像构建新镜像，通过Dockerfile添加额外依赖

相关资源

• 官方代码库：[***]
• K Framework文档：[***]
• Docker镜像仓库：[***]