The following is an extract from a system specification. It is followed by five assertions in predicate calculus. Indicate the truth or otherwise of these assertions. Also take the negation of the following assertions. “There are three types of transactions which are to be processed by the system. They are: query transactions, update transactions, and verification transactions. Two sorts of programs are allowed to issue transactions. They are: privileged programs and normal programs. Privileged programs are allowed to issue all types of transaction while normal programs are allowed to issue only query transactions. A program can be executed by any of the processors currently allocated to the system. However, if the processor is an Ia33 processor or an Ia22 processor, only update transactions are allowed.” (i) ∀ prog: programs • prog status(prog, privileged) mv prog status(prog, normal). (il) ∀prog: programs • prog status(prog, privileged) => issue(prog, update) v issue(prog, verify) v issue(prog, query). (iii) ∀prog: programs • (running(prog, Ia33) v running(prog, Ia22)) ∧ (prog_status(prog, normal) => issue(prog, update)). (iv) ∀prog: programs • ¬running(prog, Ia33) =>issue(prog, query). (v) ∀prog: programs • ¬running(prog, Ia33) ∧ ¬running(prog, Ia22) ∧ prog_status(prog, privileged) => issue(prog, update)
The following is an extract from a system specification. It is followed by five assertions in predicate calculus. Indicate the truth or otherwise of these assertions. Also take the negation of the following assertions. “There are three types of transactions which are to be processed by the system. They are: query transactions, update transactions, and verification transactions. Two sorts of
Step by step
Solved in 2 steps
