isq量子程序设计与验证平台-亚博88体育

　　isq平台是基于软件所量子软件团队多年来在量子程序设计模型、量子程序逻辑、量子程序分析算法等方面所取得的系统性理论成果基础上成功实现的。该平台包括量子程序设计、编译、模拟、分析与验证等系列工具，已上线的功能主要包括编译器、模拟器、模型检测工具、定理证明器四部分。

   近年来，随着量子计算机硬件的迅速发展，量子软件开发越来越引起人们的重视。正如相应的工具链在传统软件开发中的作用一样，一套可用性高、功能广泛而强大，集程序设计、测试、分析、验证于一体的工具链对量子软件开发十分重要。但由于量子软件与经典软件存在本质不同，相应的量子软件工具更加复杂而难以研发。

   isq平台包含的编译器能首先将高级语言编写的量子程序转化为指令集语言，然后交由模拟器、模型检测工具等后续工具进一步处理。模拟器可在经典计算机上模拟运行量子程序，查看运行结果，对现阶段量子程序的设计、测试有重要作用。模型检测工具可用于检测量子系统的各种性质。定理证明器实现了团队提出的量子hoare逻辑，是目前世界上唯一能够对量子程序是否正确进行验证的平台，可在经典计算机上克服计算时间与存储空间限制，为较大规模量子程序的设计提供重要帮助。

   isq平台支持isq编程语言。isq编程语言是由中国科学院软件研究所开发的量子程序设计语言，目前开发团队正与中科弧光量子软件公司共同研发isq语言新功能。开发团队实现了多个版本的编译器以将isq语言对接到不同的硬件平台或模拟器上，如isq-core编译器。