我试图证明Selection排序的正确性，在这种情况下，我应该仅使用数学谓词逻辑来证明程序的正确性，我发现很难将下面给出的英语语句作为谓词编写并继续进行遵循推理规则的正确性证明，

@Autowired
private SessionFactory sessionFactory;

Transaction tx = null;

public SessionFactory getSessionFactory() {
    return sessionFactory;
}

public void setSessionFactory(SessionFactory sessionFactory) {
    this.sessionFactory = sessionFactory;
}
@Override
public TmCardacceptor saveCardacceptor(TmCardacceptor cardacceptor) {
    // TODO Auto-generated method stub

    // Acquire session
    Session session = sessionFactory.openSession();
    // Save employee,saving behavior get done in a transactional manner
    //session.save(cardacceptor); //previous method
    try {


        tx = session.beginTransaction();
        session.save(cardacceptor); 
        tx.commit();


    } catch (hibernateexception e) {
        try{
        tx.rollback();
    }catch(RuntimeException rbe){
    }
    throw e;
    } finally{
        if(session!=null){
            session.close();
        }
    }

    return cardacceptor;        

}

@Override
public Term saveTerm(Term term) {
    // TODO Auto-generated method stub

    // Acquire session
    Session session = sessionFactory.openSession();
    // Save employee,saving behavior get done in a transactional manner
    //session.save(cardacceptor); //previous method
    try {


        tx = session.beginTransaction();
        session.save(term); 
        tx.commit();


    } catch (hibernateexception e) {
        try{
            System.out.println("Rolling back Term");
        tx.rollback();
    }catch(RuntimeException rbe){
    }
    throw e;
    } finally{
        if(session!=null){
            session.close();
        }
    }

    return term;        

}

我必须在谓词中编写的语句是

1. void sort(int [] a,int n) { for (int i=0; i<n-1; i++) { int best = i; for (int j=i; j<n; j++) { if (a[j] < a[best]) { best = j; } } swap a[i] and a[best]; } } 已排序

2. a[0...i-1]中的所有条目都大于或等于a[i..n-1]中的条目。