Specification and formal verification of fuzzy information processing for the case of edge detection