Formalization of Interactive Generic Algorithm