Optimization, Specification and Verification of the Prefix Sum Program in an OpenCL Environment