C$++,$ Visual Studio. I have a project with three headers and a $.$cpp file. The project is supposed to implement and test $8$ cases. Currently it only tests $4.$ It needs to test the distinction between directed and undirected adjacency lists and adjacency matrices. After the remaining tests are implemented I would appreciate if you could look at two loops or iterations and prove the correctness of them by commenting a invariant statement and showing where the invariant is true initially, the execution of the loop preserves the invariant, the invariant captures the correctness of the algorithm, and the loop terminates. I would appreciate any help, especially a practical example, and I would greatly appreciate comments so I can learn from your answer.

Driver.cpp:

#include

#include "AdjacencyMatrixGraph.h$"$

#include "AdjacencyListGraph.h$"$

int main$()\{$

AdjacencyMatrixGraph matrixGraph$(5)$;

matrixGraph.add$(0,1,1)$;

matrixGraph.add$(0,2,2)$;

matrixGraph.add$(1,3,3)$;

matrixGraph.add$(2,4,4)$;

std::cout $<<$ "Adjacency Matrix Graph: $"<<$ std::endl;

matrixGraph.display$()$;

std::cout $<<$ "Number of vertices: $"<<$ matrixGraph.getNumVertices$()<<$ std::endl;

std::cout $<<$ "Number of edges: $"<<$ matrixGraph.getNumEdges$()<<$ std::endl;

AdjacencyListGraph listGraph$(5)$;

listGraph.add$(0,1,1)$;

listGraph.add$(0,2,2)$;

listGraph.add$(1,3,3)$;

listGraph.add$(2,4,4)$;

std::cout $<<"$

Adjacency List Graph:" $<<$ std::endl;

listGraph.display$()$;

std::cout $<<$ "Number of vertices: $"<<$ listGraph.getNumVertices$()<<$ std::endl;

std::cout $<<$ "Number of edges: $"<<$ listGraph.getNumEdges$()<<$ std::endl;

return $0$;

$\}$

GraphInterface.h:

#ifndef $\_$GRAPH$\_$INTERFACE

#define $\_$GRAPH$\_$INTERFACE

template

class GraphInterface $\{$

public:

virtual int getNumVertices$()$ const $=0$;

virtual int getNumEdges$()$ const $=0$;

virtual void add$($LabelType start, LabelType end, int weight $=1)=0$;

virtual bool remove$($LabelType start, LabelType end$)=0$;

virtual int getEdgeWeight$($LabelType start, LabelType end$)$ const $=0$;

virtual void display$()=0$;

$\}$;

#endif

AdjacencyListGraph.h:

#ifndef $\_$ADJACENCY$\_$LIST$\_$GRAPH

#define $\_$ADJACENCY$\_$LIST$\_$GRAPH

#include

#include

#include

#include "GraphInterface.h$"$

template

class AdjacencyListGraph : public GraphInterface $\{$

private:

int numVertices;

std::unordered$\_$map$>>$ adjacencyList;

public:

AdjacencyListGraph$($int numVertices$)$ : numVertices$($numVertices$)\{\}$

int getNumVertices$()$ const override $\{$

return numVertices;

$\}$

int getNumEdges$()$ const override $\{$

int count $=0$;

for $($const auto& pair : adjacencyList$)\{$

count $+=$ pair.second.size$()$;

$\}$

return count;

$\}$

void add$($LabelType start, LabelType end, int weight $=1)$ override $\{$

adjacencyList$[$start$].$push$\_$back$($std::make$\_$pair$($end$,$ weight$))$;

$//$To only use directed graphs replace line $39$ with the following: adjacencyList$[$end$].$push$\_$back$($std::make$\_$pair$($start$,$ weight$))$;

$\}$

bool remove$($LabelType start, LabelType end$)$ override $\{$

auto& neighbors $=$ adjacencyList$[$start$]$;

for $($auto it $=$ neighbors.begin$()$; it $!=$ neighbors.end$()$; $++$it$)\{$

if $($it$->$first $==$ end$)\{$

neighbors.erase$($it$)$;

return true;

$\}$

$\}$

return false;

$\}$

int getEdgeWeight$($LabelType start, LabelType end$)$ const override $\{$

for $($const auto& neighbor : adjacencyList.at$($start$))\{$

if $($neighbor$.$first $==$ end$)\{$

return neighbor.second;

$\}$

$\}$

return std::numeric$\_$limits::max$()$; $//$ Edge doesn't exist

$\}$

void display$()$ override $\{$

std::cout $<<$ "Adjacency List:" $<<$ std::endl;

for $($const auto& pair : adjacencyList$)\{$

std::cout $<<$ pair.first $<<"$: $"$;

for $($const auto& neighbor : pair.second$)\{$

std::cout $<<"("<<$ neighbor.first $<<","<<$ neighbor.second $<<")"$;

$\}$

std::cout $<<$ std::endl;

$\}$

$\}$

$\}$;

#endif

AdjacencyMatrixGraph.h:

#ifndef $\_$ADJACENCY$\_$MATRIX$\_$GRAPH

#define $\_$ADJACENCY$\_$MATRIX$\_$GRAPH

#include

#include

#include

#include "GraphInterface.h$"$

template

class AdjacencyMatrixGraph : public GraphInterface $\{$

private:

int numVertices;

std::vector$>$ matrix;

public:

AdjacencyMatrixGraph$($int numVertices$)$ : numVertices$($numVertices$)\{$

matrix.assign$($numVertices$,$ std::vector$($numVertices$,$ std::numeric$\_$limits::max$()))$;

$\}$

int getNumVertices$()$ const override $\{$

return numVertices;

$\}$

int getNumEdges$()$ const override $\{$

int count $=0$;

for $($int i $=0$; i $<$ numVertices; $++$i$)\{$

for $($int j $=0$; j $<$ numVertices; $++$j$)\{$

if $($matrix$[$i$][$j$]!=$ std::numeric$\_$limits::max$())\{$

count$++$;

$\}$

$\}$

$\}$

return count;

$\}$

void add$($LabelType start, LabelType end, int weight $=1)$ override $\{$

matrix$[$start$][$end$]=$ weight;

$//$To use undirected graphs uncomment the following: matrix$[$end$][$start$]=$ weight;

$\}$