Lecture Formal methods in software engineering - Lecture 28 presents the following content: Functions, key search, binary search functions, program construction, constructing conditional statements, output variables, ghost variables, simultaneous assignment statements,. | 1 1 Formal Methods in Software Engineering Lecture # 28 1 1 1 2 2 2 2 2 3 3 Functions Find the index of the minimum value in a function First write pre and post condition and then proof You need to pass the size of the array to function Any Conditions on the input? There is no specific condition to apply on input Pre-condition: True . Any array of integer with any size Post condition: ? 3 3 3 4 4 Functions Function min ( X: in INTEGER_ARRAY) Return INTEGER Pre: True Post: j in X’First X’Last : min (X) = X (j) and i in X’First X’Last: min (x) <= X (i) and X = X’’ 4 4 4 Ada programming syntax J is an index between the first and last index When this function is executed then is there any change in the array Min(x)- value return by the function . It return value which is present in array at some index 5 5 Functions You need to specify that what would happen to the input array ( . Any change after function execution) The returning value will be the small among all but also The return value exists in the given set Question: If any of the specification component missing then ? 5 5 5 6 6 Another example We have an array and we want to find a key and want to determine that key is present or not. If present then return index – If key is not present then message not found Pre-condition ( any condition on input)? No Condition Post condition? Need to answerer some questions (about input and output array: Do we make any changes in array so X = X’’ What about the key ( what is returning): Key found or not found. 6 6 6 7 7 Key search example Pre: True Post: (( found and X (index) = key ) or ( N NOT found and ( j in X’First X’Last : x (j) not equal key )) and ( X = X’’) 7 7 7 Found and theat is present at the index 8 8 Another example Suppose we have a sorting function then array would modified? You have noted that until now, no condition is imposed on input so the pre-condition is true Restriction on input: any case? If I want to apply . | 1 1 Formal Methods in Software Engineering Lecture # 28 1 1 1 2 2 2 2 2 3 3 Functions Find the index of the minimum value in a function First write pre and post condition and then proof You need to pass the size of the array to function Any Conditions on the input? There is no specific condition to apply on input Pre-condition: True . Any array of integer with any size Post condition: ? 3 3 3 4 4 Functions Function min ( X: in INTEGER_ARRAY) Return INTEGER Pre: True Post: j in X’First X’Last : min (X) = X (j) and i in X’First X’Last: min (x) <= X (i) and X = X’’ 4 4 4 Ada programming syntax J is an index between the first and last index When this function is executed then is there any change in the array Min(x)- value return by the function . It return value which is present in array at some index 5 5 Functions You need to specify that what would happen to the input array ( . Any change after function execution) The returning value will be the small among .
