CSE 321 Homework 10

1. Provide an implementation for the two global functions Program_Occurrence_Count and Statement_Occurrence_Count specified below. Informally, Program_Occurrence_Count returns the number of calls to instruction inst in Program p, and Statement_Occurrence_Count returns the number of calls to instruction inst in Statement s. Hint: In implementing Program_Occurrence_Count you should use Statement_Occurrence_Count.

       math definition PROGRAM_OCCURRENCE_COUNT (
   	    p: PROGRAM
   	    i: string of character
   	): integer is
   	STATEMENT_OCCURRENCE_COUNT (p.body, i) +
   	CONTEXT_OCCURRENCE_COUNT (p.context, i)
   
       math definition STATEMENT_OCCURRENCE_COUNT (
   	    s: STATEMENT
   	    i: string of character
   	): integer satisfies
   	there exists label: STATEMENT_LABEL,
   		     nested_stmts: string of STATEMENT
   	    (s = compose (label, nested_stmts) and
   	     if (label.kind = CALL) and (label.instruction = i)
   	     then
   		 STATEMENT_OCCURRENCE_COUNT (s, i) = 1
   	     else
   		 STATEMENT_OCCURRENCE_COUNT (s, i) =
   		     STRING_STATEMENT_OCCURRENCE_COUNT (nested_stmts, i))
   
       math definition STRING_STATEMENT_OCCURRENCE_COUNT (
   	    str: string of STATEMENT
   	    i: string of character
   	): integer satisfies
   	if str = empty_string
   	then
   	    STRING_STATEMENT_OCCURRENCE_COUNT (str, i) = 0
   	else
   	    there exists s: STATEMENT, rest: string of STATEMENT
   		(str = <s> * rest and
   		 STRING_STATEMENT_OCCURRENCE_COUNT (str, i) =
   		     STATEMENT_OCCURRENCE_COUNT (s, i) +
   		     STRING_STATEMENT_OCCURRENCE_COUNT (rest, i))
   
       math definition CONTEXT_OCCURRENCE_COUNT (
   	    c: CONTEXT
   	    i: string of character
   	): integer satisfies
   	if c = empty_set
   	then
   	    CONTEXT_OCCURRENCE_COUNT (c, i) = 0
   	else
   	    there exists n: IDENTIFIER, s: STATEMENT
   		((n, s) is in c and
   		 CONTEXT_OCCURRENCE_COUNT (c, i) =
   		     STATEMENT_OCCURRENCE_COUNT (s, i) +
   		     CONTEXT_OCCURRENCE_COUNT (c - {(n, s)}, i))
   
       global_function Integer Program_Occurrence_Count (
   	    preserves Program& p,
   	    preserves Text inst
   	);
       /*!
   	ensures
   	    Program_Occurrence_Count = PROGRAM_OCCURRENCE_COUNT (p, inst)
       !*/
   
       global_function Integer Statement_Occurrence_Count (
   	    preserves Statement& s,
   	    preserves Text inst
   	);
       /*!
   	ensures
   	    Statement_Occurrence_Count =
                   STATEMENT_OCCURRENCE_COUNT (s, inst)
       !*/