isQ量子程序設計與驗證平臺
文章來源:量子軟件團隊 | 發布時間:2021-08-10 | 【打印】 【關閉】
isQ平臺是基于軟件所量子軟件團隊多年來在量子程序設計模型、量子程序邏輯、量子程序分析算法等方面所取得的系統性理論成果基礎上成功實現的。該平臺包括量子程序設計、編譯、模擬、分析與驗證等系列工具,已上線的功能主要包括編譯器、模擬器、模型檢測工具、定理證明器四部分。
近年來,隨著量子計算機硬件的迅速發展,量子軟件開發越來越引起人們的重視。正如相應的工具鏈在傳統軟件開發中的作用一樣,一套可用性高、功能廣泛而強大,集程序設計、測試、分析、驗證于一體的工具鏈對量子軟件開發十分重要。但由于量子軟件與經典軟件存在本質不同,相應的量子軟件工具更加復雜而難以研發。
isQ平臺包含的編譯器能首先將高級語言編寫的量子程序轉化為指令集語言,然后交由模擬器、模型檢測工具等后續工具進一步處理。模擬器可在經典計算機上模擬運行量子程序,查看運行結果,對現階段量子程序的設計、測試有重要作用。模型檢測工具可用于檢測量子系統的各種性質。定理證明器實現了團隊提出的量子Hoare邏輯,是目前世界上唯一能夠對量子程序是否正確進行驗證的平臺,可在經典計算機上克服計算時間與存儲空間限制,為較大規模量子程序的設計提供重要幫助。
isQ平臺支持isQ編程語言。isQ編程語言是由中國科學院軟件研究所開發的量子程序設計語言,目前開發團隊正與中科弧光量子軟件公司共同研發isQ語言新功能。開發團隊實現了多個版本的編譯器以將isQ語言對接到不同的硬件平臺或模擬器上,如isQ-core編譯器。
相關文檔: