现今计算机和互联网技术的迅速发展不仅带来了具有更强计算能力的计算机、更加便捷的信息交流方式，而且也对计算机软件的安全性和可靠性提出了更高的要求。目前软件安全性的保证主要是依靠程序设计者自身的能力以及软件测试。在软件开发过程中使用形式化方法进行程序验证是提高软件安全性的一个有效途径。 出具证明编译器是近些年来结合程序设计和程序验证技术所出现的研究方向。作为验证编译研究的一个分支，出具证明编译器的主要设计思想是整个系统能够在编译获得目标代码的同时也为这些目标代码生成用于说明目标代码满足某些程序性质的证明。 本文所介绍的工作基于我们的出具证明编译器原型系统项目，是我们进行出具证明编译研究的一次尝试。原型系统的设计和实现主要涉及到编译器技术、基于Hoare逻辑的程序验证技术等。此外，为了更好地考察与动态存储管理相关的程序性质，我们不仅在源语言的设计中保留了指针类型以及动态存储管理的语句，而且也设计了指针逻辑。 本文重点介绍了出具证明编译器原型系统中主要功能模块的实现，这些模块包括位于原型系统前端的验证条件生成器，位于后端的代码生成器和证明生成器。文中不仅描述了这些模块所使用的数据结构的设计以及它们各自的工作流程，而且也对设计和实现这些模块的过程中的经验进行了总结。同时，由于目标代码级程序性质证明框架的实现使用了定理证明辅助工具Coq，因此原型系统在设计和实现的过程中也加入了与Coq系统接口问题的考虑。 通过整个原型系统的构建，我们初步解决了出具证明编译中的若干问题，特别是源语言级验证条件以及目标代码级证明的生成问题。构建原型系统中积累的经验和教训可以为今后完善出具证明编译器提供很好的借鉴。