Ich habe noch weniger als eine Woche übrig und bin leider immer noch nicht fertig :(. Bis zum 01.12. habe ich sicher noch einige lange Nächte vor mir, aber es ist noch zu schaffen. Aber woran arbeite ich eigentlich?
Also mal ganz vereinfacht und an einem Beispiel erklärt geht es darum, dass aus einem Diagramm wie diesem hier (ein Visueller Kontrakt)
Spec#-Code erzeugt werden soll, der in etwa (die Beispiele sind nicht 100%ig gleich) so aussieht:
1 public Guid AddCartItem(System.Guid cartId, System.Guid productId, System.Int32 quantity)
2 requires
3 exists
4 {
5 Product product in this.ProductList;
6 Helper.IsEqual(product.ProductId, productId)
7 && exists
8 {
9 Cart cart in this.CartList;
10 Helper.IsEqual(cart.CartId, cartId)
11 && !exists
12 {
13 CartItem cartItem in cart.Items;
14 (cartItem.Product == product)
15 && Helper.IsEqual(cart.CartId, cartId)
16 }
17 }
18 };
19 ensures
20 exists
21 {
22 Product product in this.ProductList;
23 Helper.IsEqual(product.ProductId, productId)
24 && exists
25 {
26 Cart cart in this.CartList;
27 exists
28 {
29 CartItem cartItem in cart.Items;
30 (cartItem.Product == product)
31 && (cartItem.Quantity == quantity)
32 && Helper.IsEqual(cart.CartId, cartId)
33 }
34 }
35 };
36 {
37 // Code...
38 }
Der Code aus diesem Beispiel wurde schon so generiert, allerdings noch nicht aus dem Diagramm oben (das wird wahrscheinlich die Studienarbeit von Martin) sondern aus einem Objektmodell was das obige Diagramm repräsentiert. Mehr dazu blogge ich wenn ich (endlich) fertig bin.