正在加载图片...
“mcs”-2018/6/6一13:43一page8一#16 Chapter I What is a Proof? For a computer scientist,some of the most important things to prove are the correctness of programs and systems-whether a program or system does what it's supposed to.Programs are notoriously buggy,and there's a growing community of researchers and practitioners trying to find ways to prove program correctness. These efforts have been successful enough in the case of CPU chips that they are now routinely used by leading chip manufacturers to prove chip correctness and avoid some notorious past mistakes. Developing mathematical methods to verify programs and systems remains an active research area.We'll illustrate some of these methods in Chapter 5. 1.2 Predicates A predicate can be understood as a proposition whose truth depends on the value of one or more variables.So"n is a perfect square"describes a predicate,since you can't say if it's true or false until you know what the value of the variable n happens to be.Once you know,for example,that n equals 4,the predicate becomes the true proposition"4 is a perfect square".Remember,nothing says that the proposition has to be true:if the value of n were 5,you would get the false proposition"5 is a perfect square.” Like other propositions,predicates are often named with a letter.Furthermore,a function-like notation is used to denote a predicate supplied with specific variable values.For example,we might use the name"P"for predicate above: P(n):=“n is a perfect square”, and repeat the remarks above by asserting that P(4)is true,and P(5)is false. This notation for predicates is confusingly similar to ordinary function notation. If P is a predicate,then P(n)is either true or false,depending on the value of n. On the other hand,if p is an ordinary function,like n2+1,then p(n)is a numerical quantity.Don't confuse these two! 1.3 The Axiomatic Method The standard procedure for establishing truth in mathematics was invented by Eu- clid,a mathematician working in Alexandria,Egypt around 300 BC.His idea was to begin with five assumptions about geometry,which seemed undeniable based on direct experience.(For example,"There is a straight line segment between every“mcs” — 2018/6/6 — 13:43 — page 8 — #16 Chapter 1 What is a Proof?8 For a computer scientist, some of the most important things to prove are the correctness of programs and systems—whether a program or system does what it’s supposed to. Programs are notoriously buggy, and there’s a growing community of researchers and practitioners trying to find ways to prove program correctness. These efforts have been successful enough in the case of CPU chips that they are now routinely used by leading chip manufacturers to prove chip correctness and avoid some notorious past mistakes. Developing mathematical methods to verify programs and systems remains an active research area. We’ll illustrate some of these methods in Chapter 5. 1.2 Predicates A predicate can be understood as a proposition whose truth depends on the value of one or more variables. So “n is a perfect square” describes a predicate, since you can’t say if it’s true or false until you know what the value of the variable n happens to be. Once you know, for example, that n equals 4, the predicate becomes the true proposition “4 is a perfect square”. Remember, nothing says that the proposition has to be true: if the value of n were 5, you would get the false proposition “5 is a perfect square.” Like other propositions, predicates are often named with a letter. Furthermore, a function-like notation is used to denote a predicate supplied with specific variable values. For example, we might use the name “P” for predicate above: P .n/ WWD “n is a perfect square”; and repeat the remarks above by asserting that P .4/ is true, and P .5/ is false. This notation for predicates is confusingly similar to ordinary function notation. If P is a predicate, then P .n/ is either true or false, depending on the value of n. On the other hand, if p is an ordinary function, like n 2C1, then p.n/ is a numerical quantity. Don’t confuse these two! 1.3 The Axiomatic Method The standard procedure for establishing truth in mathematics was invented by Eu￾clid, a mathematician working in Alexandria, Egypt around 300 BC. His idea was to begin with five assumptions about geometry, which seemed undeniable based on direct experience. (For example, “There is a straight line segment between every
<<向上翻页向下翻页>>
©2008-现在 cucdc.com 高等教育资讯网 版权所有