A Practical Theory of Programming [PROGRAM THEORY]Department of Computer Science (Computer programming 01 beginners)Clara Jeiel [Computer Scientist, PH.D] PROGRAM THEORY We start with a very basic computational model. A computer's memory can be observed for its contents or current condition. We supply an initial state, also known as a prestate, as our input to a computation. The final state, or post state, is the result of the computation after a period of time. We only need to group the bits and see them through a code in order to perceive the memory contents to be a string of any items, even though they may actually be a string of bits. A state σ(sigma) may, for example, be given by σ = –2; 15; “A”; 3.14 The indexes of the items in a state are usually called “addresses”. The bunch of possible states is called the state space. For instance, the state space could be int; (0,..20); char; rat When the memory is in state, the things in memory are σ0 , σ1 , σ2 , and so on. We find it much more easier to refer to entities in memory by separate names such as i, n, c, and x rather than addresses. state variables are names used to refer to elements in the state. We must constantly declarewhat state variables are and what domains they belong to, but we do not state which address a state variable refers to. Formally, there is a function address that specifies the location of each state variable. For example, x = σ address “x” A state is then an assignment of values to state variables. The values are subsequently assigned to state variables. Our previous example state space was limitless,which is ridiculous; all physical memory is finite. This break from reality is tolerated as a simplification; the theory of integers is simpler than the theory of integers modulo 232, and the theory of rational numbers is significantly easier than the theory of 32-bit floating-point numbers. We must decide which aspects of the world to consider in the design of any theory and which to leave to other theories. We arefree to construct and use increasingly intricate ideas as needed, but we will face difficulties without taking into account the finite limitations of physical memory. To begin this chapter, we will solely consider the prestate and the importance of the poststate of memory Later in this class, we'll talk about execution time and shifting space requirements, and in Class 9, we'll talk about intermediate states and communication during a computation. However, for the time being, we will just consider an initial input and a final output.The issue of computation termination is a matter of execution time; termination simply indicates that the execution time is finite. The final output of a terminating calculation is available after a fixed time; in the case of a nonterminating computation, the final output is never available, or, to put it another way, it is available at time infinity. All further termination discussions have been postponed until we discuss execution time.- SPECIFICATION A specification is a binary statement with variables corresponding to quantities of interest. We are specifying computer behavior, and the quantities of interest (for the time being) are the prestate and the poststate. As input, we supply a prestate. A computer then computes and outputs a poststate. A computer must offer a satisfactory poststate to meet a specification. In other words, the specification must be met by the given prestate and the computed poststate. When the specification defines (is true of) every computation, we have an implementation. To be implementable, a specification must include at least one good output state for each input state. Here are four definitions based on the number of satisfactory outputs for each input. Specification S is unclassifiable for prestate σ : ¢(§σʹ· S) < 1 Specification S is certifiable for prestate σ :. ¢(§σʹ· S) ≥ 1 Specification S is deterministic for prestate σ : ¢(§σʹ· S) ≤ 1 S Specification S is nondeterministic for prestate σ : ¢(§σʹ· S) > 1 ∃σʹWe can rewrite the definition of certifiable as follows: Specification S is certifiable for prestate σ :. ∃σʹ· SAnd finally, Specification S is implementable:. ∀σ· ∃σʹ· SFor convenience, we prefer to write specifications in the initial values x , y , ... and final values xʹ , yʹ, ... of some state variables (we make no typographic distinction between a state variable and its initial value). Here is an example. Suppose there are two state variables x and y each with domain int . Then xʹ = x+1 ∧ yʹ=y specifies the behavior of a computer that increases the value of x by 1 and leaves y unchanged. Let us check that it is implementable. We replace ∀σ by either ∀x, y or ∀y, x and we replace ∃σʹ by either ∃xʹ, yʹ or ∃yʹ, xʹ ; according to the Commutative Laws, the orderdoes not matter. We find ∀x, y· ∃xʹ, yʹ· xʹ = x+1 ∧ yʹ=y One-Point Law twice =∀x, y· ⊤ Identity Law twice = ⊤This requirement is met by a computation that increases x by any amount while leaving y unchanged or changing it to any integer. For each initial state, this specification is nondeterministic. Computer behavior that meets the earlier specification x' = x+1^ y’ = y also meets this one, although there are many methods to meet this one that do not meet the earlier one. In general, weaker specifications are easier to implement than stronger specifications. At one extreme, we have the specification ; it is the simplest specification to implement because ⊤it is satisfied by all computer behavior. The specification , on the other hand, is impossible to ⊥implement because it is not satisfied by any computer behavior. However, ⊥is not the only specification that cannot be implemented. Here’s another one. x≥0 ∧ yʹ=0 the starting value of x is not a negative number, the specification can be met by setting variable y to0. However, if the initial value of x is negative, the specification cannot be met. Maybe the specifier doesn’t want to provide a negative input; in that case, the specifier should have written: x≥0 ⇒ yʹ=0