(******
*
* Module GradedItems is made to hold the gradebook
*
*)


module GradedItems;

from NewClass import StatsBar;
export all;

object Gradebook is
	components: MarkList and aStatsBar and studentList and classInfo;	
	
	object MarkList is Mark*;
	description: (* Contains all of the valid marks for a gradebook *);
	end MarkList;
	
	object aStatsBar is StatsBar;
	description: (* Stats bar linked to students graded items *);
	end aStatsBar;

	object studentList is Student*;
	description: (* The complete list of all students in the class *);
	end studentList;
	
	object classInfo is 
		components: professor and term and year and course and section;
	
	
			object professor is string;
			description:(* Name of the professor teaching the class *)
			end professor;

			object term is Fall or Winter or Spring;
			description: (* Quarter of the year it is *);
			end term;
	
			object year is integer;
			description: (* Year in format yyyy *);
			end year;

			object course is string;
			description: (* Course number and major i.e. "CSC 205" *);
			end course;
	
			object section is integer;
			description: (* Two digit indicator of the section of a specific course *);
			end section;

	description: (* Collection of information related to a specific class *);
	end classinfo;
	
	
	description: (* The gradebook item contains a list of students each
	with their own graded items *);
end Gradebook;

object Student is
	components: name and id and total and grade and classwork;
	
	object name is string;
	description: (* Students first and last name *);
	end name;

	object id is integer;
	description: (* Students ID number *);
	end id;

	object total is color and points;
		
		object points is real;
		description: (* Number of total points *);
		end points;

		object color is Color;
		description: (* Color of text *);
		end color;

	description: (* Students total percentage grade *);
	end total;

	object grade is color and points;
		object points is real;
		description: (* Number of total points *);
		end points;

		object color is Color;
		description: (* Color of text *);
		end color;
	description: (* Students letter grade *);
	end grade;

	object classwork is Category;
	description: (* Collection of students work.  By default classwork.catName will be "Classwork" *);
	end classwork;
	
	description: (* A student in a class along with all the info a gradebook needs to display about them *);
end Student;

object Category is
	
	components: subcategory and item and catName and catMaxPoints and catWeight and
	catLateIntvl and catLateAmnt and catDecay and catGraceDays and catElecTurnin and
	catExtraCredit and catNotes;

	object subcategory is Category*;
	description: (* A collection of subcategories below the current category *);
	end subcategory;

	object item is Item*;
	description: (* A collection of items in the current category *);
	end item;

	object catName is string;
	description: (* Name referencing the current category *);
	end catName;

	object catMaxPoints is real;
	description: (* The maximum number of points for all the items in the category *);
	end catMaxPoints;
	
	object catWeight is real;
	description: (* If relative grading is defined the % weight of the category toward the overall grade *);
	end catWeight;

	object catLateIntvl is none or Hours: or Days: or Weeks: or Months:;
	description: (* The interval that the integer in catLateAmnt is multiplied by for the total late period *);
	end catLateIntvl;

	object catLateAmnt is integer;
	description: (* Integer that when multiplied by catLateIntvl speicifies total late period *);
	end catLateAmnt;

	object catDecay is real;
	description: (* Number of points lost by items ,in this category by default, every late period *);
	end catDecay;

	object catGraceDays is integer;
	description: (* Number of days to wait ,in this category by default, before starting a late period *);
	end catGraceDays;

	object catElecTurnin is bool;
	description: (* Allows/Disallows electronic turn-in for this category *);
	end catElecTurnin;

	object catExtraCredit is real;
	description: (* Number of extra credit points by default on items in this category *);
	end catExtraCredit;

	object catNotes is string;
	description: (* Any additional description a user would like to add about the category *);
	end catNotes;


	description: (* A category can contain further subcategories or graded items which
	represent an organization for student's graded items *);

end Category;

object Item is
	components: itemName and itemCurPoints and itemMaxPoints and itemWeight and
	itemLateIntvl and itemLateAmnt and itemDecay and itemGraceDays and itemElecTurnin and
	itemExtraCredit and itemNotes and itemDueDate and itemAssignDate and itemColor;
	
	object itemName is string;
	description: (* Name referencing the current item *);
	end itemName;

	object itemPoints is real;
	description: (* Current points the student scored on this item *)
	end itemPoints;

	object itemMaxPoints is real;
	description: (* The maximum number of points for this item *);
	end itemMaxPoints;

	object itemWeight is real;
	description: (* If relative grading is defined the % weight of this item toward the overall grade *);
	end itemWeight;

	object itemLateIntvl is none or Hours: or Days: or Weeks: or Months:;
	description: (* The interval that the integer in itemLateAmnt is multiplied by for the total late period *);
	end itemLateIntvl;

	object itemLateAmnt is integer;
	description: (* Integer that when multiplied by itemLateIntvl speicifies total late period *);
	end itemLateAmnt;

	object itemDecay is real;
	description: (* Number of points lost on this item every late period *);
	end itemDecay;

	object itemGraceDays is integer;
	description: (* Number of days to wait before starting a late period *);
	end itemGraceDays;

	object itemElecTurnin is bool;
	description: (* Allows/Disallows electronic turn-in for this item *);
	end itemElecTurnin;

	object itemExtraCredit is real;
	description: (* Number of extra credit points obtainable for this item*);
	end itemExtraCredit;

	object itemNotes is string;
	description: (* Any additional description a user would like to add about the item *);
	end itemNotes;

	object itemDueDate is string;
	description: (* The date mm/dd/yyyy an item is due*);
	end itemDueDate;

	object itemAssignDate is string;
	description: (* The date mm/dd/yyyy an item was assigned*);
	end itemAssignDate;

	object itemColor is Color;
	description: (* Color of item points *);
	end itemColor;

	description: (* Items are the final sub level of the graded item hierarchy and contain
	the pertinent information regarding assignments. *);
end Item;

object Mark is markName and markValue;
	
	object markName is string;
	description: (* The name or symbol used to represent a mark *);
	end markName;
	
	object markValue is real;
	description: (* The value of a mark *);
	end markValue;

	description: (* Symbol used to represent a percentage value *);
end Mark;
	
object Color is Red or Blue or Black;
object Red;
object Blue;
object Black;
description: (* Color for text *);
end Color;

object none;
object Hours:;
object Days:;
object Weeks:;
object Months:;


operation Add is
	inputs: parentCat:Category,newItem:Item,gb:Gradebook;
	outputs: gb':Gradebook;
	precondition:(forall(i:integer | i>0 and  i< #(parentCat.item))
				 	newItem.itemName != parentCat.item.itemName 
					newItem.itemWeight >= 0 and newItem.itemWeight <= 100
					newItem.itemDeacy <= newItem.itemMaxPoints
			 )
	(* Item of the same name can't already exist in the given Category
	   Item values must be within the specified range *);
	postcondition: (exists(gb':Gradebook)
			   	(forall(i:integer | i>0 and i< #(parentCat.item))
					(exists(parentCat.item == newItem))
				)
			   )
	(* Gradebook must contain the new Item *);
	description: (*Adds an item to a specified Category in the Gradebook *);
end Add;

operation Add is
	inputs: parentCat:Category,newCat:Category,gb:Gradebook;
	outputs: gb':Gradebook	;
	precondition: (forall(i:integer | i>0 and  i< #(parentCat.subcategory))
				 	newCat.catName != parentCat.subcategory.catName 
					newCat.catWeight >= 0 and newCat.catWeight <= 100
					newCat.catDeacy <= newCat.catMaxPoints
			  )
	(* Category of the same name can't already exist in the given Category,
	Category values must be within the specified range *);
	
	postcondition: (forall(i:integer | i>0 and i< #(parentCat.subcategory))
					(exists(parentCat.subcategory == newCat))
			   )
	(* Gradebook must contain the new Catgory *);
	description: (*Adds a Category to a specified Category in the gradebook*);

end Add;

operation Edit is
	inputs: item:Item,gb:Gradebook;
	outputs: gb':Gradebook;
	precondition: item.itemWeight >= 0 and item.itemWeight <= 100
			  item.itemDeacy <= item.itemMaxPoints
	(* changes made to Item must be within specified ranges *);
	postcondition: (* Gradebook must update the Item *);
	description: (*Edits an items values in the gradebook*);

end Edit;

operation Edit is
	inputs: cat:Category,gb:Gradebook;
	outputs: gb':Gradebook;
	precondition: cat.catWeight >= 0 and cat.catWeight <= 100
			  cat.catDeacy <= cat.catMaxPoints
	(* changes made to Category must be within specified ranges *);
	postcondition: (* Gradebook must update the Category *);
	description: (*Edits a categories values in the gradebook*);
end Edit;

operation Remove is
	inputs: item:Item,gb:Gradebook;
	outputs: gb':Gradebook;
	precondition: (* Valid item must be selected *);
	postcondition: (* Gradebook must remove the Item *);
	description: (*Removes an item from the gradebook*);
end Remove;

operation Remove is
	inputs: item:Catgory,gb:Gradebook;
	outputs: gb':Gradebook;
	precondition: (* Valid Category must be selected *);
	postcondition: (* Gradebook must remove the Category *);
	description: (*Removes a Category from the gradebook*);
end Remove;

operation EditCurrentPoints is
	inputs: numPoints:real,item:Item,gb:Gradebook;
	outputs: gb':Gradebook;
	precondition: numPoints <= (item.itemMaxPoints + item.itemExtraCredit)
	(*The new number of points must be below the max points and extra credit*);
	postcondition: item.itemPoints == numPoints
	(* Gradebook must contain the updated point value for the Items itemPoints *);
	description: (* Edits a students assignment score *);
end EditCurrentPoints;


end GradedItems;