CSE 321 Homework 8

Consider the specifications for Number_Of_Primitive_Instructions. Informally, Number_Of_Primitive_Instructions returns the total number of calls in Statement s to any of the primitive instructions (move, skip, turnright, turnleft, infect)

    math definition IS_PRIMITIVE_INSTRUCTION (
            inst: IDENTIFIER
        ): boolean satisfies
        inst is in ("move", "skip", "turnright", "turnleft", "infect")

    math definition NUMBER_OF_PRIMITIVE_INSTRUCTIONS (
            s: STATEMENT
        ): integer satisfies
        there exists label: STATEMENT_LABEL,
                     nested_stmts: string of STATEMENT
            (s = compose (label, nested_stmts) and
             if (label.kind = CALL) and 
                (IS_PRIMITIVE_INSTRUCTION (label.instruction))
             then
                 NUMBER_OF_PRIMITIVE_INSTRUCTIONS (s) = 1
             else if (label.kind = CALL) then
                 NUMBER_OF_PRIMITIVE_INSTRUCTIONS (s) = 0
             else
                 NUMBER_OF_PRIMITIVE_INSTRUCTIONS (s) =
                     STRING_NUMBER_OF_PRIMITIVE_INSTRUCTIONS (nested_stmts))

    math definition STRING_NUMBER_OF_PRIMITIVE_INSTRUCTIONS (
            str: string of STATEMENT
        ): integer satisfies
        if str = empty_string
        then
            STRING_NUMBER_OF_PRIMITIVE_INSTRUCTIONS (str) = 0
        else
        there exists s: STATEMENT, rest: string of STATEMENT
            (str = <s> * rest and
             STRING_NUMBER_OF_PRIMITIVE_INSTRUCTIONS (str) =
                 NUMBER_OF_PRIMITIVE_INSTRUCTIONS (s) +
                 STRING_NUMBER_OF_PRIMITIVE_INSTRUCTIONS (rest))

    global_function Integer Number_Of_Primitive_Instructions (
            preserves Statement& s
        );
    /*!
        ensures
            Number_Of_Primitive_Instructions = 
                NUMBER_OF_PRIMITIVE_INSTRUCTIONS (s)
    !*/

Give the value of Number_Of_Primitive_Instructions(s), if the value of s is

Assume you have an implementation of the following global function:

    global_function Boolean Is_Primitive_Instruction (
        preserves Text& inst
    );
    /*!
    ensures
         Is_Primitive_Instruction = 
         IS_PRIMITIVE_INSTRUCTION (inst)
    !*/

Provide an implementation for the global function Number_Of_Primitive_Instructions.