微计算机信息
微計算機信息
미계산궤신식
CONTROL & AUTOMATION
2008年
12期
233-234,237
,共3页
程序不变量%不变量动态发现%编配工具哌
程序不變量%不變量動態髮現%編配工具哌
정서불변량%불변량동태발현%편배공구고
程序不变量是用于描述程序运行过程中某些保持不变的性质的逻辑断言.程序编配的任务是通过对程序改造,暴露程序的运行轨迹,然后在通过对轨迹分析完成程序不变量的发现.程序编配是程序不变量过程中的关键步骤.本文介绍了C程序编配的工作原理和主要方法,并详细说明了采用内嵌法的编配工具的设计过程.
程序不變量是用于描述程序運行過程中某些保持不變的性質的邏輯斷言.程序編配的任務是通過對程序改造,暴露程序的運行軌跡,然後在通過對軌跡分析完成程序不變量的髮現.程序編配是程序不變量過程中的關鍵步驟.本文介紹瞭C程序編配的工作原理和主要方法,併詳細說明瞭採用內嵌法的編配工具的設計過程.
정서불변량시용우묘술정서운행과정중모사보지불변적성질적라집단언.정서편배적임무시통과대정서개조,폭로정서적운행궤적,연후재통과대궤적분석완성정서불변량적발현.정서편배시정서불변량과정중적관건보취.본문개소료C정서편배적공작원리화주요방법,병상세설명료채용내감법적편배공구적설계과정.
