计算机工程与科学
計算機工程與科學
계산궤공정여과학
COMPUTER ENGINEERING & SCIENCE
2010年
9期
84-88,94
,共6页
循环不变式%PAR方法%高可靠性软件%谓词抽象
循環不變式%PAR方法%高可靠性軟件%謂詞抽象
순배불변식%PAR방법%고가고성연건%위사추상
高可靠性软件是当今软件开发的热点问题.确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键.循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一.本文研究了众多现有循环不变式开发方法中较为典型的几种方法,指出了它们的基本原理、技术难点、特点及效果,旨在探寻循环不变式本质特征,从而为研究更简单、有效的生成方法提出指导.
高可靠性軟件是噹今軟件開髮的熱點問題.確保算法程序邏輯結構正確最理想的途徑是算法程序的形式化推導和證明,而循環不變式是算法程序形式推導和證明的關鍵.循環不變式的開髮一直是算法程序設計領域中最具挑戰性、最富有創造性、也是最睏難的問題之一.本文研究瞭衆多現有循環不變式開髮方法中較為典型的幾種方法,指齣瞭它們的基本原理、技術難點、特點及效果,旨在探尋循環不變式本質特徵,從而為研究更簡單、有效的生成方法提齣指導.
고가고성연건시당금연건개발적열점문제.학보산법정서라집결구정학최이상적도경시산법정서적형식화추도화증명,이순배불변식시산법정서형식추도화증명적관건.순배불변식적개발일직시산법정서설계영역중최구도전성、최부유창조성、야시최곤난적문제지일.본문연구료음다현유순배불변식개발방법중교위전형적궤충방법,지출료타문적기본원리、기술난점、특점급효과,지재탐심순배불변식본질특정,종이위연구경간단、유효적생성방법제출지도.
