Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods