Supponiamo che il seguente tipo sia definito (la sintassi C ++, può essere concettualmente applicata a qualsiasi linguaggio tipizzato staticamente.)
class T {
int val;
friend bool operator<(const T& lhs, const T& rhs) {
return lhs.val < rhs.val;
}
// Ideally, if we should make them "friends"
// Also, this doesn't make them belong to the type itself as they're not member functions
friend bool operator>=(const T& lhs, const T& rhs) {
return !(lhs < rhs);
}
// Also the following implementation is interesting
friend bool operator>=(const T& lhs, const T& rhs) {
return lsh.val >= rhs.val;
}
};
Quindi, il compilatore può sicuramente verificare se T supporta l'operatore < oppure operator > =, può solo cercare la dichiarazione.
Questo diventa più complicato se questi fossero definiti come "amici" invece di funzioni membro, ma può essere fatto per quanto mi riguarda.
Tuttavia, il compilatore può controllare se l'"assioma comune di ordinamento" è valido? (Come in è possibile verificarlo in tutti gli scenari? Non importa se questo sarebbe conforme allo standard.) Dire:
non (a < b) == a > = b
Dovremmo definirne uno in termini di altro, è sicuramente possibile in questo particolare scenario, ma questo non è naturalmente l'unico assioma da controllare, per quanto riguarda:
(a > b) = > (b < a)
e inoltre non è necessario (sfortunatamente) definire il nostro comportamento in termini di qualcosa che è già stato definito. E a volte non sarebbe nemmeno possibile.
Quindi, se il compilatore può controllare se certi assiomi valgono, come? Generare valori casuali da determinati intervalli? È possibile ideare e verificare la correttezza di tali intervalli?
Questo è principalmente legato ai concetti C ++ che, a differenza dei concetti C ++, dovrebbe anche essere in grado di "supportare gli assiomi", qualunque cosa significhi, non riesco a vedere un modo chiaro su come possono essere applicati. O il creatore del tipo deve dichiarare quali assiomi obbedisce alla sua classe? C ++ ha abbandonato le "mappe concettuali" per quanto ne so.