這裏的賦值項是控製路線上的分枝語句所取的邏輯值。控製路線上的最後一個語句不包括在這些賦值項和邏輯條件之內。借助謂詞演算，可以用機器來產生驗證條件。
究竟什麼是結構程序設計，有著不同的說法。有人曾將結構程序設計定義為這樣一種設計，借助於這一設計方法可以使得在測試的每一階段中，需要測試的情形的數目都減到很少，從而可以對所有情形進行測試。另外有人則將它定義為能使編出來的程序容易維護的設計方法。後一種定義失之於過於寬泛。
現在我們來看一下結構程序設計究竟有一些什麼特點。一般認為結構程序設計有下列兩個特點：具有層次結構；對用到的控製結構的種類作適當的限製，特別是限製轉向語句的使用，從而使得編出來的程序能夠少犯邏輯錯誤和容易修改。兩種控製結構都是不用轉向語句的。
在理論上第一種控製結構已經足夠，促加上分情形語句等三種結構，效率可以提島。還有，重要的是要限製控製結構中那些容易產生邏輯錯誤的結構，而這樣的結構並非僅限於轉向語句。另一方麵，轉向語句也一定在所有情形中都會使程序變得晦澀難懂，而且行時不用轉語句對效率影響很大，在這種情形中還是應該用轉向語句。
近年來，西方國家有軟件設作者在有軟件中應用高階軟件技術。我們認為，軟件就是遵守一組形式規則，用軟件的記語出的軟件（他們將這種形式規則稱為“公理”，因此，這種技術也可以稱之為公理方法）。
他們製定了六條規則。規則避免發生邏輯錯誤的規則。他們認為如果一個程序沒有違反這六條規則，則可以保證其中不會包含有常見的邏輯錯誤（似不能保證其中沒有任何邏輯錯誤）。他們研製：係統專門用來檢查一個特定的程序是否違反了這幾條規則。他們曾將這一技術應用於天空實驗室和探測外行星的宇宙飛船的控製程序獲得了良好的效果。他們發展的這一技術是值得重視的。
測試與證明
對於正確性證明這一方法的有效性是有懷疑意見的。首先是在1976年提出了一種他稱之為“程序的邏輯分析”的方法。他認為正確性證明的缺陷在於其隻能應用於沒有邏輯錯誤的程序，而對於有邏輯錯誤的程序卻無能為力。他提出了一種對程序進行邏輯分析的方法，他說這種方法對包含有邏輯錯誤的程序將能夠查出錯誤，並指出這些錯誤存在於哪些程序塊中；而對沒有邏輯錯誤的程序將能夠證明其正確性；但他的新方法還有待於發展。
在1975年指出，對於大程序在事後進行證明是極端困難的。他說這有些將拉車的馬不係在車前而係在車後。他認為目前程序驗證的問題是“將馬由車後牽到車前”，也就是邊設計邊驗證的方法。最近幾年所從事的“正確程序技術”就是屬於這一方向的。他們的方法是先選擇若幹經過反複調試和驗證從而可以保證沒有錯誤的程序塊作為基本程序塊（一般為幾十條指令的小程序）；再找出程序的組合規則，並且證明：從基本程序出發，按照這些規則組成的大程序是沒有邏輯錯誤的。他們認為這樣編出的程序就可以保證是基本上沒有邏輯錯誤的。
其次指出，將程序正確性的證明與數學定理的證明相比較時，可以發現前者比後者要冗長得多。這主要是由於數學定理的證明通常是依靠前麵已證明過的若幹基本定理而不是從頭證起；而程序正確性的證明卻是從頭證起。這個問題在60年代末已有人發現和討論過，但這些年來情況沒有多大變化。指出了這一問題。
他們說，程序正確性證明的鼓吹者以為程序的證明可以和數學定理的證明有同樣的可站性，而實際情況遠非如此。他們認為，數學定理的證明實際上是一種社會過程。一個數學家在證明了-一條定理之後，常常是先告訴幾個同行，征求他們的意見。在這些人認為這個定理是有意義的以後，他就會在一個討論班:報告這一結果。在乂得到好的反時，他就去寫成論文，打印若幹份送給一些人征求意見，在再度得到積極的反應以後，他才向專門學報投稿。最後是對這篇論文提出修改意見，作者寫出修改稿，然後這篇論文終於發喪，這時常要經過幾年的時間。然而他們認為這樣的一種過程對程序的證明說來是不可能有的，當時它也就不可能具有數學定理證明那樣的可靠性。他們並且認為。
我們認為，人的分析中有一些深刻的見解，但他們認為程序正確性證明注定要失敗的看法卻是未必正確的。在他們看來，數學定理的證明必須經過人的審稿才能被認為是正確的。我們認為這種看法是難以成立的因為這不僅涉及程序正確性證明而涉及定理的機械化證明。四色定理的證明就是由人來審稿的，後來他們發表在《伊利諾伊大學數學學報》上的論文據說是由機器“審稿”的。因此如果堅持數學定理的可靠性必須完全由人的審稿來保證，是會遇到難以克服的困難的。