의사 코드의 전제 조건 작성 방법

Question

의사 코드에서 사전 조건을 나타내는 방법을 알고있는 사람이 주변을 둘러 보았으므로이 주제에 대해 아무 것도 찾을 수 없다는 것을 알고 있었는지 궁금했습니다.

, 당신에게

Answer 1

의사 코드를 감사, 정의에 의해 는 코드를 공식화되지 않습니다. C#을 방법의 전제 조건을 정의하는 의사 코드를 사용하는 예는 다음과 같습니다 의사 코드 정형화되지 않으므로

// Precondition: Object must have been initialized by calling init() or by 
// manually setting properties X and Y such that X.Foo >= Y.Bar. 
public void doUsefulWork() { 
    ... 
} 

분명히,이 컴파일러에 의해 검증 될 수 없다. (일반적으로)

• IT는 전제 조건이 충족되는 것을 보장하기위한 방법의 사용자의 듀티, 그리고
• 은 그 전제 조건을 변경하는 것을 인정하는 방법의 현상의 의무 큰 변화.

Answer 2

내가 여기 두 가지 가능성을 참조 : 당신이 진짜 코드로 당신의 조건을 수립 할 수있는 경우

1. 을, 나는 Programming With Assertions 시도 (또는 .NET 동등한 Debug.Assert)을 줄 것입니다. 이 방법을 사용하면 런타임 중에 조건을 점검 할 수 있습니다. assert condition

2. 이 경우가 아니면 원하지 않는 경우 JavaDoc에 사전 및 사후 조건을 쓸 수 있습니다.

   /** 
   * @precondition: the connection has been established. 
   * 
   * @postcondition: the schema is created. 
   * 
   */ 
   

심지어 이러한 JavaDoc annotations을 정의 할 수는 그래서 그들은 javadoc에 생성 된 문서에 나타납니다. 자연어를 사용하여 주장하고자하는 것을 정의 할 수 있습니다.

또한 더 수학적으로 내가 그들을 더 이해 할 수 귀하의 조건의 간결, 향상시키기 위해 당신의 사전 및 사후 조건을 표현할 수있다 :

당신은 분명히 사용할 수있는 단순한 숫자 비교의 경우를 <, <=, >, 등 >=, 그러나의 당신은 다음과 같은 그것을 표현할 수있는 Set의 불변을 정의하려면 가정 해 봅시다 :

따라서 당신의 상태를 표현하는 가상/의사 기능을 활용

/** 
    * @invariant: set == filterDuplicates(set) 
    * 
    */ 

.

기능 언어가 더 마음에 들면 더 발전시킬 수 있습니다. 내 데이터 구조 및 알고리즘 교수는 새로 도입 된 데이터 구조에 대한 전제 조건, 사후 및 불변을 정의 할 에게 하스켈를 사용 :

module TreeSets(TreeSet, 
       contains, add, remove, card, traverse) 
where 
data Ord t => TreeSet t = E | N (TreeSet t) t (TreeSet t) 

inv E = True 
inv(N l x r) = all(<x)(abs l) && all(>x)(abs r) && 
    inv l && inv r 

정말 따라 당신이 작성하는 누구를 위해, 따라서 나의 추천 자연 언어를 사용하는 것입니다 . 모든 사람이 이해할 수 있으며 특별히 객체 지향 프로그램이 가장 쉬운 방법입니다.