C++ preconditions /斷言

這不是我的家庭作業 - 我只是在練習。我似乎無法圍繞這個斷言概念進行思考。C++ preconditions /斷言

1) Determine the pre-condition for x that guarantees the post-condition about y 
{ _______ } 
if (x > 0) 
    y = x; 
else 
    y = -x; 

{ y >= 0 && |y| == |x| } 
2) This code is the same as has been seen before, but the post-condition is different.      
Describe why this post-condition is better for verifying the code than just { y >= 0}.

來源

2013-02-28 erbisme4

從發佈條件反向工作。只有一個分支語句。由於if語句測試x> 0，那麼只需查看3種情況：x < 0,x == 0和x > 0以確定x的哪些值滿足後置條件。

來源

2013-02-28 04:28:54 stark

我猜想，因爲通常整數類型可以表示從（-N）> 0>（N-1）。也就是說，如果你的int是32位有符號整數，它可以保存值-2147483648，但不是值2147483648

{X！= INT_MIN}

來源

2013-02-28 04:33:53

如果你這樣做是爲了瞭解編程，你可以做一個位編程，以幫助您確認了答案：

#include <iostream> 

int abs(int x) { return x >= 0 ? x : -x; } 

int main() 
{ 
    for (int i = -128; i <= 127; ++i) 
    { 
     char x = i; 

     char y; 

     if (x > 0) 
      y = x; 
     else 
      y = -x; 

     if (!(y >= 0 && abs(y) == abs(x))) 
      std::cout << "failed for " << i << " (y " << (int)y << ")\n"; 
    } 
}

運行此你會看到，如果失敗了x -128（其中y爲-128）。這是由於2的補碼錶示中的不對稱：-128可以用8位字符表示，但128不能（只有127）。

因此，對於1，假設2的補碼整數，前提條件是x不是位寬度中最低的可表示值。當然，這個問題中沒有什麼可以說x和y都是整數，所以這些都是暫時的。

如果x和y是浮點或雙精度說，然後在正常IEEE表示有，可以在不影響尾數或指數，讓標誌的「乾淨」的變化進行切換符號位。也就是說，也有「不是數字」（NaN）和（正和負）無限哨兵價值的角落案例，這是明智的檢查實驗和/或通過研究表示和行爲規範....

描述爲什麼[{y> = 0 & & | y | == | x | }]比驗證代碼更好，而不僅僅是{y> = 0}。

一個模糊的問題，因爲我們對代碼試圖實現什麼沒有把握，而且我們對此的推理來自於前一種後置條件優於後者的斷言。儘管如此，他們正在尋找一個答案：前者還確保y的絕對量級能夠存活，無論代碼所做的符號更改是否爲x。

實際上，對於我們的2的補碼整數，幅度在之後總是匹配 - 這是標記角落情況的後置條件的符號部分。但是，對預期內容有更多的瞭解仍然令人放心。

來源

2013-02-28 04:51:39

根據x和y的類型，答案可能會變得混亂。正如@PeteFordham所指出的那樣，二進制補碼中的整數不是對稱的，不能表示最大負值的絕對值。如果不是整數x和y是float或double那麼你必須考慮在IEEE格式中，零可以同時具有正號和負號。

#include <iostream> 
int main() { 
    double x = 0; 
    double y = -x; 
    std::cout << "x=" << x << " y=" << y << std::endl; 
}

輸出是

x = 0時Y = -0

來源

2013-02-28 04:56:48 amdn

如果x> 0，Y> = 0總是由於if (x > 0) y = x滿足。如果x == 0，y> = 0始終滿足if (x > 0) ... else y = -x。如果x < 0，則y = -x所以y> = 0是滿足的，除非-x < 0.所以前提條件是{x> = 0 || -x> = 0}。（其中x不唯一的值是最大負值，其溢出）。

{y> = 0 & & | y | == | x | }比{y> = 0}更好，因爲後者對於各種函數都是正確的，而不僅僅是找到x的絕對值（這可能是這個代碼的用途，儘管你似乎忽略了重要的部分問題陳述）。

來源

2013-02-28 05:15:48

C++ preconditions /斷言

回答

相關問題