tailieunhanh - Lecture Introduction to Computer Programming - Lecture 22

In this section, we introduce the features of JML as they apply to the formal specification and verification of an individual function, such as the Factorial function that we specified and verified by hand in the previous section. We also show how JML allows us to specify run-time exceptions, providing a more robust vehicle than the pure Hoare triples in a real computational setting where exceptions actually occur. | CSC141- Introduction to Computer programming Teacher: AHMED MUMTAZ MUSTEHSAN Lecture – 22 Thanks for Lecture Slides: Principles of Programming - NI2005 Strings in C No explicit type, instead strings are maintained as arrays of characters Representing strings in C stored in arrays of characters array can be of any length end of string is indicated by a delimiter, the zero character ‘\0’ String Literals String literal values are represented by sequences of characters between double quotes (“) Examples “” - empty string “hello” “a” versus ‘a’ ‘a’ is a single character value (stored in 1 byte) as the ASCII value for a “a” is an array with two characters, the first is a, the second is the character value \0 Referring to String Literals String literal is an array, can refer to any single character from the literal as a character Example: printf (“%c”,”hello”[1]); outputs the character ‘e’ During compilation, C creates space for each string literal (digit of characters in the literal + 1 for null terminator) Referring to the literal refers to that location (as if it is an array) Duplicate String Literals Each string literal in C program is stored at a different location So even if the string literals contain the same string, they are not same/equal (in the == sense) Example: char string1[6] = “hello”; char string2[6] = “hello”; but string1 may be similar to string2 but string1 is not the same as string2 (they are stored at different locations) String Variables Allocate an array of a size large enough to hold the string (plus 1 extra value for the delimiter) Examples (with initialization): char str1[6] = “Hello”; char str2[] = “Hello”; char *str3 = “Hello”; char str4[6] = {‘H’,’e’,’l’,’l’,’o’,’\0’}; Note, each variable is considered a constant in terms of its size as that the allocated space to it cannot be changed str1 = str2; /* not allowable, but we can copy the contents of str2 to str1 */ Pointer and . | CSC141- Introduction to Computer programming Teacher: AHMED MUMTAZ MUSTEHSAN Lecture – 22 Thanks for Lecture Slides: Principles of Programming - NI2005 Strings in C No explicit type, instead strings are maintained as arrays of characters Representing strings in C stored in arrays of characters array can be of any length end of string is indicated by a delimiter, the zero character ‘\0’ String Literals String literal values are represented by sequences of characters between double quotes (“) Examples “” - empty string “hello” “a” versus ‘a’ ‘a’ is a single character value (stored in 1 byte) as the ASCII value for a “a” is an array with two characters, the first is a, the second is the character value \0 Referring to String Literals String literal is an array, can refer to any single character from the literal as a character Example: printf (“%c”,”hello”[1]); outputs the character ‘e’ During compilation, C creates space for