用Petri網描述程序精化中的循環不變式

Petri網于60年代由德國物理學家PetIi在其博士論文中提出，故而稱為Petri網，最開始這是一種網狀結構來模擬通信系統，目前Petfi網理論已經得到很大的發展，其應用已涉及計算機科學的各個領域，如軟件工程、人工智能、形式語義、操作系統等。已經證明Petri網的模擬能力與圖靈機等價”。