PL/0语言实现
PL/0 语言是 Pascal 语言的设计者 Niklaus Wirth 在其专著 Algorithms + Data Structures = Programs 一书（译著书名：算法＋数据结构＝程序）中给出的一个小巧的高级语言。PL/0 是 Pascal 语言的一个子集，常被用于编译原理的教学实践。
PL/0 语言编译器的实现分成两部分，把源语言翻译成中间语言的编译器和中间语言解释器。编译器用的是递归下降的预测分析方法。中间语言是一种栈机器代码，其指令集是根据 PL/0 语言的需要来设计的。解释器是编译器中的一个过程，若源程序无错，则编译结束时调用解释过程 interpret。
编译器对 PL/0 源程序进行一遍扫描，并逐行输出源程序。在源程序无错的情况下，编译器每编译完一个分程序，就列出该分程序的代码。
Niklaus Wirth 设计的编译器是用 Pascal 语言编写的，为教学方便，在尊重 Niklaus Wirth 的原意的基础上，《编译原理与技术》（高等教育出版社，2010.8）一书的作者陈意云教授和张昱副教授用 C 语言对代码进行了改写。这里给出的是对PL/0编译器的C语言实现的验证。
根据编译功能，程序被分成了词法分析、语法分析等多个文件。由于验证器学习版目前只支持单个文件的验证，所以，读者在将C程序文件提交给验证器进行验证之前，需手动将头文件的有关宏定义和变量声明展开到验证文件的头部。
有关验证的说明：科创验证器学习版目前只支持单文件的验证，用户自定义的头文件在验证之前须手动展开。
（相关文件下载：PL0.h、specification.h 和 pl0_init.c）
Examples of verified algorithms