Zėŋōfōbìå

17 gennaio 2009

Design by Contract

Filed under: C#, DbC, informatica — Tag:, — Zeno @ 19:41

Chiacchierando con JP sul suo blog, cercando di parlare male dei linguaggi che ci danno da vivere, siamo incappati nella questione del DbC.

Design By Contract (DbC) è una tecnica di programmazione adottata per la prima volta dal linguaggio Eiffel, che permette di definire delle condizioni a contorno del codice che debbano essere garantite durante tutta la sua esecuzione. I linguaggi e le estensioni che ammettono il DbC in genere permettono di definire:

– precondizioni : condizioni in entrata di funzione, possono essere dei limiti sulle variabili in ingresso.

– postcondizioni : garanzie fornite in uscita di funzione, che definiscono, per esempio, l’insieme dei valori d’uscita ed eventuali side effect.

– invarianti : certezze che devono essere mantenute durante l’esecuzione (per esempio il limite sui side effects)

Interessante il fatto che, in presenza di ereditarietà, le precondizioni degli ancestor possono essere strette, le postcondizioni allargate.

Questa tecnica sembra essere pronta per una rinascita, dal momento che sia il C++ che C# si stanno evidentemente preparando ad estendersi in questa direzione.

C++0x, infatti, incorpora i “concept”, che sono una estensione dei templates, certamente utili per fornire, tramite tecniche di metaprogrammazione, robusti metodi formali per garantire la correttezza del codice.

C#, a sua volta, pare che nella versione 4 incorpori una libreria, chiamata Code Contract Library, che è già disponibile al download. (Allego il contractsmanual  )

Ovviamente, simulare il DbC usando l’equivalente delle ASSERT del C, è possibile, in parte limitante, certamente inefficace: se la garanzia formale di correttezza venisse garantita staticamente i vantaggi sarebbero enormi. Un buon DbC effettuerà una parte di controlli staticamente, il resto runtime.

Come funziona il controllo statico? Questa è la domanda che più mi incuriosisce e mi immagino che la risposta sia sufficientemente interessante da farmi provare questa tecnica appena possibile.

Installando la CCL (Microsoft Research), oltre all’installazione della libreria e della documentazione pdf, viene integrato in VS2008 uno strumento atto alla gestione del DbC. In particolare, nelle propietà del progetto, viene aggiunta una nuova sezione, che permette di abilitare:

– dynamic check (con la possibilità di definire delle asserzioni implicite)

– static check.

Se si costruisce un metodo che ha tra le precondizioni un valore maggiore di 0 e gli si passa un valore negativo il DbC statico identifica il problema. (Spesso basterebbe aver modo di definire i range dei tipi, come in Ada , io credo, e avere un controllo statico sui boundaries. ).

Se per esempio una funzione con una postcondizione che limita l’ouput ad un intero minore di 10 viene passata come argomento ad una funzione che tra le precondizioni vuole un intero maggiore di 10, possiamo immaginare che esiste un possibile controllo statico che blocchi la compilazione di fronte a questa incongruenza.

Ho provato ad installare la libreria e a scrivere questo snippet:

internal double logarithm(double c)
{
  CodeContract.Requires(c  > 0);
  return Math.Log(c);
}

internal double negative(double a)
{
  CodeContract.Ensures(CodeContract.Result<double>() <= 0 );
  if (a > 0)
    return (-a);
  else
    return a;
}

Mi aspetterei un errore alla riga dove scrivo :

double c=logarithm(negative(123.0));

E in effetti ho un warning: requires unproven

Cioè viene detto che non è certo che i requisiti in ingresso del logaritmo siano provati.

Ovviamente ottengo l’errore runtime, ma, francamente mi aspettavo un errore un po’ più visibile.

Probabilmente la tecnologia è ancora troppo sperimentale, o forse non ho usato la keyword giusta, ma d’altra parte, mi pare che non sia ancora possibile scrivere un programma che sappia esprimersi sulla correttezza di un altro programma. ;-)

L’implementazione della libreria, per la parte runtime, è molto semplice, non aggiunge più overhead di quello di un’assert e l’impatto nella versione di release è praticamente nullo.

Credo quindi che abbia senso utilizzarla fin da adesso, se non altro per favorire la documentazione.

Annunci

18 marzo 2008

Parsing internazionale di numeri

Filed under: C#, informatica — Tag: — Zeno @ 8:44

Il parsing delle stringhe è un problema legato all’internazionalizzazione del codice ma anche all’interfacciamento di ambienti diversi. Tipicamente un server in inglese ed uno in italiano comunicheranno le proprie informazioni con stringhe diverse. A prescindere dal fatto che, la dove
possibile occorra usare una codifica indipendente dalla lingua, la soluzione fornita da .Net è la seguente:

1 int.Parse(“32.768”);
2 int.Parse(“32,768”, System.Globalization.NumberFormatInfo.InvariantInfo);

14 dicembre 2007

Natural Sort in C#

Filed under: C#, informatica — Tag: — Zeno @ 14:20

Natural Sort in sei righe, tratto da: http://www.nbdtech.com/Blog/

Il Natural Sort è l’ordinamento delle stringhe che ci appare naturale quando le stringhe contengono numeri.

Normalmente, infatti, ordinando secondo lo standard alfanumerico una lista che contenga stringhe nella forma : “1_elem”,”2_elem”, … ,”100_elem” avviene che il 100_elem viene anteposto al 2_elem, fornendo un’ordinamento diverso da quello che ci saremmo aspettati.

La soluzione più semplice che ho trovato è la seguente:

  1 [DllImport("Shlwapi.dll", CharSet = CharSet.Unicode)]
  2 private static extern int StrCmpLogicalW(string psz1, string psz2);

Una volta richiamato il collegamento alla funzione esterna si può passare al Array.Sort:

  3 Array.Sort(myStringArray, delegate(string l, string r)
  4 {
  5       return StrCmpLogicalW(l, r);
  6 });

15 novembre 2007

Compatibilita dei Thread con C# 2.0

Filed under: C#, informatica, Linguaggi — Tag:, , , — Zeno @ 10:18

Fare il porting di una applicazione Windows Form C# 1.1 verso C# 2.0 comporta delle modifiche impegnative. Una delle difficoltà da affrontare riguarda il fatto che con C# 2.0 non è più possibile, da parte di un Thread diverso da quello di una certa form, di accedere ai suoi componenti grafici.

Le soluzioni sono due: correggere tutti gli accessi con degli Invoke oppure settare un flag di compatibilità con 1.1:

CheckForIllegalCrossThreadCalls = false;

4 aprile 2007

Delegati e Invoke in C# 2.0

Filed under: C#, informatica — Tag:, , , — Zeno @ 13:22

Il primo impatto con C# 2.0, tipicamente, è negativamente legato all’impossibilità di invocare dei metodi da thread differenti con un approccio diretto.

Supponiamo da un thread di dover modificare la label della form principale, segue una soluzione estremamente semplice:

myLabel.Invoke((MethodInvoker)delegate
{
    myLabel.Text = "What a great post";
});

24 marzo 2007

Gestire i log con log4net

Filed under: C#, informatica — Tag:, — Zeno @ 11:01

Ho sempre dedicato una fetta del tempo di sviluppo di qualunque applicazione di un certo rilievo alla realizzazione di una libreria di log che fosse comoda e adatta alle esigenze del programma. In genere quello che occorre è sempre uguale: una routine che permetta di salvare su un file, piuttosto che in un sql, un insieme di informazioni che comprenda: data del log, entità del problema, thread, riga del file di codice (ammesso che sia possibile), messaggio.
Mi è capitato più di una volta di perdere del tempo per una cattiva implementazione della libreria, alla quale non si vuole dedicare mai troppo tempo.

Sto provando Log4Net, soluzione di Apache che mi pare eccellente. Modulare, configurabile, comoda, semplice, è una meraviglia.

Un esempio per chiarirne la comodità:

using log4net;
using log4net.Config;

...
static class Program
{
    private static readonly ILog log =
        LogManager.GetLogger(MethodBase.GetCurrentMethod().DeclaringType);

    static void Main()
    {
        // Set up a configuration taken from xml.
        XmlConfigurator.Configure(new System.IO.FileInfo("logfile.xml"));

        log.Info("Main");
    }
}

Notate che non viene determinata la forma del log: questa è descritta nel file xml logfile.xml, che contiene:

<?xml version="1.0" encoding="utf-8" ?>

<log4net>
  <appender name="RollingFile" type="log4net.Appender.RollingFileAppender">
    <file value="filelog.log" />

    <appendToFile value="true" />
    <maximumFileSize value="1000KB" />
    <maxSizeRollBackups value="10" />

    <layout type="log4net.Layout.PatternLayout">
      <conversionPattern value="%date [%thread] %-5level %logger (%file:%line) - %message%newline" />
    </layout>

  </appender>

  <root>
    <level value="DEBUG" />
    <appender-ref ref="RollingFile" />

  </root>
</log4net>

In questa maniera vengono creati dei file di nome myproject.log, per un massimo di 100Kb e 20 files.
conversionPattern definisce la formattazione, che in questo caso produce log del tipo:

2007-03-22 15:27:43,923 [10] INFO Program (C:ProgettitestLog4net.cs:26) - Main

« Newer Posts

Blog su WordPress.com.