Abstract: The problem of across river is a classical problem in artificial intelligence. The algorithms or programs which have been proposed before are not formalized. Their correctness can not be guaranteed. Generally, these algorithms or programs can only provide particular solution. This paper generalizes the problem above by applying program transformation and properly selecting parameters and filters(logic expression) to guarantee equation recursion and to improve algorithm efficiency, and finally, compeletely-formally derives all solutions which are expressed as correct function-like recursive programs.