Formalismi per la definizione della specifiche dei sistemi software e loro applicazione alla costruzione di una libreria per la differenziazione automatica