Question For Todd Niec - Need Help Designing A Program

Question:  

What would be the pre and post conditions when writing a formal specification.  The specification would be written for a program which utilizes multiple trees to store predefined indexes in a specified order.  Each index node stores a pointer to a linked list node which in-turn stores a pointer to a data structure.

Answer:

      ************************  FORMAL SPECIFICATION  **************************

      LIST FUNCTIONS

      --------------------------   InitializeList()   ---------------------------

            void InitializeList(struct List *List)

       *      Description: This procedure initializes a linked list structure so that it
                                     defines a valid empty list, that is, a linked list with no
                                     items stored in it.

       *      Input:
                                    The parameter is a pointer to the list structure
                                    that is to be initialized

       *      Returns:     N/A

       *      Requires:       N/A

       * Precond:     N/A

       * Postcond:    The specified list structure will be altered so that it
                                       specifies a valid empty list.


      ------------------------  AddListItem()  ------------------------------

            ListNode *AddListItem(LnkLst *List, void *DataPointer)

       *      Description: This procedure stores the data specified by the 2nd parameter
                                     at the start of the list specified by the first parameter.
                                     The 2nd parameter should be a pointer to a dynamically
                                     allocated block of memory.  The list will store a pointer to
                                     this memory so it can be retreived at later times.  When the
                                     list entry added by this procedure is later deleted from the
                                     list, this block of memory will be deleted.

       *      Input              : The first parameter is a pointer to a list structure that
                                     defines the linked list to which the specified data should be
                                     added.

                                : The second parameter is a pointer to a dynamically allocated
                                     block of memory.  This list will store a pointer to this
                                     memory at the current start of the list.  The list will "own"
                                     this memory in the sense that it will preserve the memory
                                     until this item is removed from the list, then it will delete
                                     the memory.

       *      Returns        : This procedure returns a ListNode pointer that refers to the
                                     item just added.  This pointer can be passed as a parameter
                                     to several other list procedures in order to identify the
                                     particular item added to the list.

       *      Requires        : This procedure requires that the specified list structure
                                     defines a valid linked list.  The second parameter must
                                     specify a pointer to a block of dynamically allocated memory
                                     that the list may assume "ownership" for.  Since this
                                     procedure allocates memory to store the the specified data,
                                     sufficient memory must be available on the heap.

       * Precond.        : The list structure of the first parameter must be initialized
                                     as a valid list.  The pointer of the second parameter must
                                     be void in order to utilize the linked list as a generic
                                     container.  The void pointer should be initialized as a valid
                                     data structure for this program (owner, dealer, offender)

       * Postcond.  : The linked list specified by the first parameter is altered
                                     to specify a new first item in the list.  The program's heap
                                     space is diminished by the amount required to store this new
                                     item in the list.

            -------------------------   DeleteListItem() ---------------------------

        void DeleteListItem(struct List *List,struct node *NodPtr)

      * Description: This procedure deletes a specified item from a specified
                                    linked list.  The other items in the list, if any, remain in
                                    the list in their same order.  The procedure will delete the
                                    memory block that is associated with this list item, that is,
                                    it will delete the memory that was specified when the item was
                                    added to the list.

      * Input:       The first parameter is a pointer to a list structure defining
                                    the linked list from which the item is to be deleted.

                                    The second parameter is a pointer to an index node that
                                    indicates the item in the list that is to be deleted.  This
                                    pointer should be obtained from a previous call to one of the
                                    other linked list procedures.  This item must be from the
                                    same list as the list specified by the first parameter.

      * Returns:     N/A

      * Requires:    The specified list structure must define a valid linked list.
                                    The specified node ptr must specify an item that is currently
                                    stored in this specified list.  (It may not be a pointer that
                                    refers to an item in a different list and it may not be a
                                    pointer to an item that was previously removed from the list.)

      * Precond:     The specified node ptr refers to an item stored in the
                                    specified linked list.  The specified the node pointer refers
                                    (indirectly) to a block of dynamically allocated data that was
                                    specified when the item was added to the list and is now
                                    stored by the list.

      * Postcond:    The list will be altered to indicate that the specified item
                                    is no longer stored in the list.  The other items, if any,
                                    will remain in the list in their same order.  The item refered
                                    to by the specified node pointer will be deleted, so the node
                                    pointer is now invalid and thus may not be used in other
                                    list procedure calls.  The block of dynamically allocated data
                                    that wass stored by the deleted item will also be deleted and
                                    other pointers to this block of memory, if any, will now be
                                    invalid.


      ---------------------------  DeleteList()  -------------------------------

            void DeleteList(struct List *List)

       *      Description: This procedure traverses the specified list starting from
                                     the head list node and deletes each list node.  All DB record
                                     structures stored in the list are also deleted.  When this
                                     procedure returns, the list structure will specify a valid,
                                     empty linked list.

       *      Input              : The "List" parameter is a pointer to a list structure that
                                     defines the linked list whose stored data is to be deleted.
                                     When the procedure returns the linked list will be empty.
                                     The list structure will indicate that the list is empty, so
                                     it can safely be used in other list operations like adding
                                     new items to the list.

       *      Returns        : -


       *      Requires        : The linked list specified by the parameter be a valid
                                     linked list, this means that the nodes are all dynamically
                                     allocated and properly linked to each other and that the list
                                     structure points to the terminal nodes.  Each node in the
                                     linked list must have a pointer to a dynamically allocated
                                     DB record structure to be deleted by the procedure.

       * Precond.        : The list parameter points to a linked list structure
                                     specifying a list with 0 or more nodes.

       * Postcond.  : When the procedure returns, the DB records stored by the
                                     linked list will be deleted.  All of the resources used by
                                     the linked list to store the records, i.e. the dynamnically
                                     allocated nodes, will also be deleted.  The list structure
                                     will be set to indicate a valid empty list.


      -------------------------  GetFirstListItem() ---------------------------

        struct node *GetFirstListItem(const struct list *List)

      * Description: This procedure returns a node pointer that refers to the
                                    first item in the linked list.  This pointer may be passed
                                    to many of the other linked list procedures in order to
                                    specify this item to those procedures.  The list is not
                                    affected by this procedure.

      * Input:       The parameter is a pointer to a list structure defining
                                    the linked list whose first item is to be returned.

      * Returns:     A node pointer that may be used to refer to the first item
                                    in the linked list.  A NULL pointer is returned if the list
                                    is empty.

      * Requires:    The specified list structure must define a valid linked list.

      * Precond:     N/A

      * Postcond:    Nothing will be altered by this procedure.



      ------------------------- GetLastListItem() -----------------------------

        struct node *GetLastListItem(const struct list *List)

      * Description: This procedure returns a node pointer that refers to the
                                    last item in the linked list.  This pointer may be passed
                                    to many of the other linked list procedures in order to
                                    specify this item to those procedures.  The list is not
                                    affected by this procedure.

      * Input:       The parameter is a pointer to a list structure defining
                                    the linked list whose last item is to be returned.

      * Returns:     A node pointer that may be used to refer to the last item
                                    in the linked list.  A NULL pointer is returned if the list
                                    is empty.

      * Requires:    The specified list structure must define a valid linked list.

      * Precond:     N/A

      * Postcond:    Nothing will be altered by this procedure.

      -------------------------  GetNextListItem() -------------------------------

        struct node *GetNextListItem(const struct node *Node)

      * Description: This procedure returns a node pointer that refers to the
                                    next item in the linked list after the specified item refered
                                    to by the node pointer specified in the parameters.  The
                                    node pointer returned may be passed to many of the other
                                    linked list procedures in order to specify this next item to
                                    those procedures.  The list is not affected by this procedure.

      * Input:       The parameter is a pointer to a list node that refers to the
                                    item whose next item is to be returned.

      * Returns:     A node pointer that may be used to refer to the next item
                                    in the linked list.  A NULL pointer is returned if there is
                                    no next item in the list, that is, if the item specified in
                                    the parameters was the last item in the list.

      * Requires:    The specified node pointer must refer to a node in a valid
                                    linked list.

      * Precond:     N/A

      * Postcond:    Nothing will be altered by this procedure.

      ------------------------  GetPreviousListItem() ----------------------------

        struct node *GetPreviousListItem(const struct node *Node)

      * Description: This procedure returns a node pointer that refers to the
                                    previous item in the linked list before the specified item
                                    refered to by the node pointer specified in the parameters.
                                    The node pointer returned may be passed to many of the other
                                    linked list procedures in order to specify this previous item
                                    to those procedures.  The list is not affected by this
                                    procedure.

      * Input:       The parameter is a pointer to a list node that refers to the
                                    item whose previous item is to be returned.

      * Returns:     A node pointer that may be used to refer to the previous item
                                    in the linked list.  A NULL pointer is returned if there is
                                    no previous item in the list, that is, if the item specified
                                    in      the parameters was the first item in the list.

      * Requires:    The specified node pointer must refer to a node in a valid
                                    linked list.

      * Precond:     N/A

      * Postcond:    Nothing will be altered by this procedure.

      --------------------------  GetListItemData()   -------------------------

        void *GetListItemData(const struct node *Node)

      * Description: This procedure returns a pointer to the dynamically allocated
                                    block of memory that is stored by the list item that is
                                    refered to by the node poiner.  The block of memory returned
                                    is the block of memory that was specified to be stored by the
                                    list when the item was added to the linked list.  This block
                                    of memory is "owned" by the list and will be deleted when the
                                    item is removed from the list.

      * Input:       The parameter is a pointer to a list node that refers to the
                                    item whose stored memory block is to be returned.

      * Returns:     A pointer to the memory that was specified to be stored by the
                                    list when the item was added tot he linked list.

      * Requires:    The specified node pointer must refer to a node in a valid
                                     linked list.

      * Precond:     N/A

      * Postcond:    Nothing will be altered by this procedure.


      ********************* FORMAL SPECIFICATION CONTINUED ******************

      INDEX FUNCTIONS

      -------------------------- InitializeIndex() --------------------------

            void InitializeIndex(const struct Index *Index)

      *      Description: This procedure initializes an index structure so that it
                                     defines a valid empty index, that is, an index with no keys
                                     stored in it.

      *      Input:
                                     The parameter is a pointer to the index structure
                                     that is to be initialized

      *      Returns:     N/A

      *      Requires:       N/A

      *       Precond:     N/A

      *       Postcond:    The specified index structure will be altered so that it
                                     specifies a valid empty index.


       --------------------------  AddIndexItem()  ------------------------------

            BOOL AddIndexItem(const struct Index *Index, string Index, ListNodee *)

       *      Description: This function tries to add the specified index key and the
                                     associated ListNodee pointer into the specified index.  If
                                     the specified key is not already in the index, it is added to
                                     the index and the specified data pointer is stored with it,
                                     then the procedure returns true, indicating no error occured.
                                     If the specified key is already in the index, the procedure
                                     returns false to indicate an error occured.
       *      Input              :
                                     The first parameter is a pointer to the index structure
                                     defining the index that the key is supposed to be added to.

                                     The second parameter is a pointer to a NUL terminated string
                                     specifying the key to be added to the index.  This string
                                     may not be longer than MaxKeyLen characters long.  The
                                     procedure will store a copy of the specified string in the
                                     index, so the caller's copy does not need to be preserved
                                     after the procedure returns with the associated key.

                                     The third parameter ia  a 'ListNode' pointer which is stored
                                     with the associated key.  The procedure will store this
                                     pointer in the index.  So that it can be retreived by other
                                     index operations in order to access the data.

       *      Returns        : This procedure returns a boolean value that indicates if the
                                     specified key was added.  The procedure returns true if the
                                     specified key was added to the index.  The procedure returns
                                     false if the specified key was not added to the index,
                                     usually because the key was already in the index.

       *      Requires        : The index structure specifid in the first parameter must
                                     define a valid index and the key specified in the second
                                     paremaeter must specify a NUL termianted string that is not
                                     longer than MaxKeyLen charaters long.  The procedure
                                     dynamically allocates memory to store the key and associted
                                     ListNode pointer, so sufficient heap memory must be availalbe

                                     This procedure must determine whether the the input key is
                                     a duplicate, in which case it is not entered.

       * Precond.        : The first parameter to an index structure needs to be
                                     initialized.  Otherwise, the proceudre will crash when it
                                     attempts to add the index item.  The second parameter
                                     (key string) also needs to be initialied since it's contents
                                     contains the type of sort required on the associated data
                                     pointed to.  The third parameter is dereference and therefore
                                     it must be validated by this function.

       * Postcond.  : The index will be altered to store the specified key and the
                                     associated data pointer, if the key wasn't already in the
                                     index.

      -------------------------  DeleteIndexItem() -----------------------------

            void DeleteIndexItem(const struct Index *Index, const char *Key)

      *      Description: This procedure deletes the specified key and its associated
                                     list node pointer from the specifed index.  The other keys,
                                     if any, will remain in the index.  The procedure does not
                                     delete the associated list node from its linked list.

      *      Input:
                                     The first parameter is a pointer to the index structure
                                     defining the index that the key is supposed to be removed from.

                                     The second parameter is a pointer to a NUL terminated string
                                     specifying the key to be removed from the index.  This string
                                     must specify a key that is currently stored in the index.

      *      Returns:     N/A

      *  Requires:       The index specified by the index structure must be valid.
                                     The key specified must currently be stored in the index.

      *  Precond:     The specified key must be stored in the index.

      *  Postcond:    The specified key and its associated data will be removed
                                     from the index.  The memory used to store the key and its
                                     associated list node pointer in the index will be returned
                                     to the heap.


      ---------------------------   DeleteIndex()  --------------------------

            void DeleteIndex (struct Index *Index)

       * Description: This procedure empties the index, that is, it deletes every
                                     key and its associated ListNode pointer stored in the index.
                                     The procedure does not delete the ListNodes themselves, it just
                                     deletes the pointer to those ListNodes from the index.  When
                                     the procedure returns the index structure will specify a
                                     valid, empty index.

       *      Input              : This parameter is a pointer to the index structure for the
                                     index whose stored data is to be cleared.

       *      Returns        : -

       *      Requires        : The index specified must be constructed validly.

       * Precond.        : The parameter points to a valid index with 0 or more keys.

       * Postcond.  : When the procedure returns, the keys and associated ListNode
                                     pointers stored in the index will be deleted from the index.
                                     All of the resources used by the index to store the data,
                                     i.e. the dynamnically allocated index nodes, will also be
                                     deleted.  The index structure will be set to indicate a valid
                                     empty index.

            -------------------------  SearchIndexNode()  --------------------------

            ListNode * SearchIndexNode(const struct Index *Index, char * KeyValue)

       *      Description: This procedure searches the specified index for a stored key
                                     that matches the specified key.  If a matching key is found,
                                     the ListNode pointer associated with that key is returned.  If
                                     no matching key is found the procedure returns a NULL pointer


       *      Input              : The first pointer is a pointer to the index structure
                                     defining the index to be searched for the desired key.

                                     The second parameter is a pointer to a NUL terminated string
                                     specifying the search key.  This string must match the
                                     string length and type of the index type in order to be a
                                     valid search value.

       *      Returns        : If the key to be searched for was in the index, this
                                     procedure returns the ListNode pointer that is stored along
                                     with that key, otherwise, if the key was not stored in the
                                     index, the procedurreturns a NULL pointer.

       *      Requires        : That the list be valid and the search key be valid.

       * Precond.        : The first parameter must point to a index structure that
                                     defines a valid index.  The second parameter must point to a
                                     NUL terminated string.

       * Postcond.  : The return value will be used for the purpose of deleting.
                                     The specified index is not changed by this procedure


      --------------------------   GetFirstIndexItem() --------------------------

            ListNode *GetFirstIndexItem(const struct Index *Index, char *OutKey)

      *      Description: This procedure returns a pointer to the list node that is
                                     associated with the first key stored in the index.  The
                                     procedure also returns, if desired, the first key stored
                                     in the index.  The index is not altered by this procedure.

      *      Input:             The first parameter is a pointer to the index structure
                                     defining the index whose first item is to be returned.

                                     The second parameter is a pointer to a buffer that is to
                                     receive the first key in the index.  The procedure will copy
                                     copy the first key in the index to this buffer, if the index
                                     is empty, the procedure will not change this buffer.  The
                                     buffer must be sufficiently long enough to hold the specified
                                     key.  If this second parameter is NULL, the procedure will
                                     not copy the first key to the buffer.

      *      Returns:     A pointer to the list node associated with the first key in
                                     the index.  NULL will be returned if there is no first key in
                                     the index, that is, if the index is empty.

      *      Requires:       The index specified by the index structure must be valid.
                                     The buffer specified by the 2nd parameter must be
                                     sufficiently large enough to store the NUL terminated key
                                     string from the index, or the 2nd parameter must be NULL.

      * Precond:      N/A

      * Postcond:     The buffer specified by the 2nd parameter, if any, will be
                                     altered to specify the first key stored in the index.  The
                                     list will not be altered in any way.

      -----------------------  GetLastIndexItem()  -----------------------------

            ListNode *GetLastIndexItem(const struct Index *Index, char *OutKey)

      *      Description: This procedure returns a pointer to the list node that is
                                     associated with the last key stored in the index.  The
                                     procedure also returns, if desired, the last key stored
                                     in the index.  The index is not altered by this procedure.

      *      Input:
                                     The first parameter is a pointer to the index structure
                                     defining the index whose last item is to be returned.

                                     The second parameter is a pointer to a buffer that is to
                                     receive the last key in the index.  The procedure will copy
                                     copy the last key in the index to this buffer, if the index
                                     is empty, the procedure will not change this buffer.  The
                                     buffer must be sufficiently long enough to hold the specified
                                     key.  If this second parameter is NULL, the procedure will
                                     not copy the last key to the buffer.

      *      Returns:     A pointer to the list node associated with the last key in
                                     the index.  NULL will be returned if there is no last key in
                                     the index, that is, if the index is empty.

      *      Requires:       The index specified by the index structure must be valid.
                                     The buffer specified by the 2nd parameter must be
                                     sufficiently large enough to store the NUL terminated key
                                     string from the index, or the 2nd parameter must be NULL.

      * Precond:      N/A

      * Postcond:     The buffer specified by the 2nd parameter, if any, will be
                                     altered to specify the last key stored in the index.  The
                                     index will not be altered in any way.

      ----------------------------GetNextIndexItem() ---------------------------

            ListNode *GetNextIndexItem(const struct Index *Index, const char *Key,
                                                                        char *OutKey)

      *      Description: This procedure returns a pointer to the list node that is
                                     associated with the next key stored in the index after the
                                     specified key.  The procedure also returns, if desired, the
                                     key stored by this next item.  The index is not altered by
                                     this procedure.

      *      Input:             The first parameter is a pointer to the index structure
                                     defining the index whose next item is to be returned.

                                     The second parameter is a pointer to a NUL terminated string
                                     that specifies the key of the index item whose next index
                                     item is to be returned.  The key does not actually have to be
                                     stored in the index, the procedure will simply return the
                                     next key and list node pointer that occurs after the location
                                     the specified key's would have in the index.

                                     The 3rd parameter is a pointer to a buffer that is to
                                     receive the next key in the index.  The procedure will copy
                                     copy the key found in the index to this buffer, if there is
                                     no next key in the index, the procedure will not change this
                                     buffer.  The buffer must be sufficiently long enough to hold
                                     the specified key.  This buffer may be the same buffer
                                     specified by the second parameter.  If this third parameter
                                     is NULL, the procedure will not copy the key found to the
                                     buffer.

      *      Returns:         A pointer to the list node associated with the next key in
                                     the index.  NULL will be returned if there is no next key in
                                     the index after the specified key, that is, if the specified
                                     key was the last item in the index, or occurs after the last
                                     item in the index.

      *      Requires:       The index specified by the index structure must be valid.
                                     The buffer specified by the 3rd parameter must be
                                     sufficiently large enough to store the NUL terminated key
                                     string from the index, or the 2nd parameter must be NULL.

      * Precond:      N/A

      * Postcond:     The buffer specified by the 3rd parameter, if any, will be
                                     altered to specify the next key stored in the index.  The
                                     index will not be altered in any way.



John500Asked:
Who is Participating?
I wear a lot of hats...

"The solutions and answers provided on Experts Exchange have been extremely helpful to me over the last few years. I wear a lot of hats - Developer, Database Administrator, Help Desk, etc., so I know a lot of things but not a lot about one thing. Experts Exchange gives me answers from people who do know a lot about one thing, in a easy to use platform." -Todd S.

KangaRooCommented:
Is this homework?
Just kidding, looks like C rather than C++ to me though.
0
ozoCommented:
What's the distinction between Requires: and Precond: ?
0
KangaRooCommented:
Why did you delete this question?
0

Experts Exchange Solution brought to you by

Your issues matter to us.

Facing a tech roadblock? Get the help and guidance you need from experienced professionals who care. Ask your question anytime, anywhere, with no hassle.

Start your 7-day free trial
It's more than this solution.Get answers and train to solve all your tech problems - anytime, anywhere.Try it for free Edge Out The Competitionfor your dream job with proven skills and certifications.Get started today Stand Outas the employee with proven skills.Start learning today for free Move Your Career Forwardwith certification training in the latest technologies.Start your trial today
C++

From novice to tech pro — start learning today.