//function that checks if a path is good.
bool isGoodPath(char pathName[256]);

//function that receives requests
void processRequest(SOCKET sock) {
    char buffer[1024];
    recv(sock, buffer, sizeof(buffer), 0);
    char path[1024];
    extractPath(buffer, path);
    if (isGoodPath(path)) doRequest(buffer);
}

//input: {char[256]}
//output: {false, true}
bool isGoodPath(char pathName[256]);

//input: {socket}
void processRequest(SOCKET sock) {
    char buffer[1024];

    //input: {socket -> socket, char[1024] -> char*}
    //output: {char*}
    recv(sock, buffer, sizeof(buffer), 0);

    char path[1024];

    //input: {char[1024] -> char[1024]}
    //output: {char[1024]}
    extractPath(buffer, path);

    [b]//input: {char[1024] -> char[256]}[/b]
    if (isGoodPath(path)) doRequest(buffer);
}

#include <string>
#include <iostream>
#include <fstream>
using namespace std;

fstream file;

int main() {
    while (1) {
        cout << "input 1 to open the file, 2 to input string, 3 to close the file; press enter to exit\n";
        string s;
        cin >> s;
        if (s.empty()) then break;
        if (s == "1") {
            file.open("out.txt");
            if (file.is_open()) {
                cout << "file opened\n";
            }
            else {
                cout << "can not open file\n";
                break;
            }
        }
        else if (s == "2") {
            cin >> s;
            file << s;
            cout << "written: " << s << "\n";
        }
        else if (s == "3") {
            file.close();
            cout << "file closed\n";
        }
        else {
            cout << "wrong option\n";
        }
    }
    file.close();
    return 0;
}

int main() {

    //input: {file(opened or closed)}
    //output: {file(opened or closed)}
    while (1) {
        cout << "input 1 to open the file, 2 to input string, 3 to close the file; press enter to exit\n";

        string s;
        cin >> s;

        if (s.empty()) then break;

        if (s == "1") {

            [b]//input: {file(opened or closed) -> file(closed)}[/b]           
            //output: {file(opened or closed)}           
            file.open("out.txt");

            [b]//input: {file(opened or closed)}[/b]           
            //output: {file(opened)}
            if (file.is_open()) {
                cout << "file opened\n";
            }
            else {
                cout << "can not open file\n";
                break;
            }
        }

        else if (s == "2") {
            cin >> s;

            [b]//input: {file(opened or closed) -> file(opened)}[/b]           
            //output: {file(opened)}
            file << s;
            cout << "written: " << s << "\n";
        }

        else if (s == "3") {
            [b]//input: {file(opened or closed) -> file(opened)}[/b]           
            //output: {file(closed)}
            file.close();
            cout << "file closed\n";
        }

        else {
            cout << "wrong option\n";
        }
    }

    [b]//input: {file(opened or closed) -> file(closed)}[/b]
    //output: {file(closed)}
    file.close();

    return 0;
}

class File {
    FILE *m_handle = null;

    bool open(const char *file) {
        [b]assume m_handle == null;[/b]
        //bla bla open file
    }

    bool close(const char *file) {
        [b]assume m_handle != null;[/b]
        //bla bla close file
    }
}

requirement {
    record Contact {
        firstName : String;
        lastName : String;
        email : EMailAddress;
        phone : PhoneNumber;
    }    
    variable contacts : {Contact};
    operation addContact: {contacts, Contact} -> {contacts + Contact};    
    operation deleteContact: {contacts, Contact} -> {contacts - Contact};
}

    class Contact [b]implements requirement Contact[/b] {
        String firstName [b]implements requirement Contact.firstName[/b];
        String lastName [b]implements requirement Contact.lastName[/b];
        EMailAddress email [b]implements requirement Contact.email[/b];
        PhoneNumber phone [b]implements requirement Contact.phone[/b];
    }
    
    List<Contact> contacts [b]implements requirement contacts[/b];
    
    class App {
        public static void main(string[] args) {
            //bla bla build the gui
            
            //add a callback which implements the 'addContact' operation
            newContactMenuItem.setClickEvent(new ClickEvent () {
                contacts.add(new Contact) [b]implements requirement addContact[/b];
            });
            
            //add a callback which implements the 'deleteContact' operation
            deleteContactMenuItem.setClickEvent(new ClickEvent () {
                Contact contact = getCurrentContact();
                contacts.remove(contact) [b]implements requirement removeContact[/b];
            });
        }
    }

 
MyObject getSomething {
    return (some condition)? new MyObject() : null;
}

 
> MyObject getSomething {
>     return (some condition)? new MyObject() : null;
> }