QUESTION 6
For each method described below, provide a Dafny method signature and specication. If you refer to a function or predicate (i.e., boolean function) in your specication, you must provide a full denition of the function or predicate. You do not need to include a specication of any functions or predicates you dene.
Each part of the question is worth 3 marks.
(a) A method, Count, which returns the number of occurrences of an integer, x, in an integer array.
(b) A method, MaxZeroes, which returns the longest sequence of zeroes in an integer array, e.g., for array [3, 0, 0, 9, 0, 0, 0, 2, 0], the method will return 3.
(c) A method, Trim, which modies an integer array by removing all leading zeroes, e.g., the method will change the array [0, 0, 3, 0 , 9, 0] to [3, 0, 9, 0].
