Skip to content
Snippets Groups Projects
Commit b112e368 authored by Shale XIONG's avatar Shale XIONG
Browse files

Modify the navigator to two-level:

1. Add one field, parent_menu, which should have the same name as the folder name (case insensitive). For menus has the same parent_menu are supposed to have the same menu_order.
 2. Change the way to generate navigator. Now it traverses the menu_order. If it is list of menu where the first element has parent_menu, it will generate a pop-up parent menu with a list of nav. Otherwise it will generate nav as before.
parent 1c3f52b1
No related branches found
No related tags found
No related merge requests found
...@@ -22,6 +22,5 @@ ...@@ -22,6 +22,5 @@
ga('create', 'UA-47856851-3', 'auto'); ga('create', 'UA-47856851-3', 'auto');
ga('send', 'pageview'); ga('send', 'pageview');
</script> </script>
</head> </head>
...@@ -2,15 +2,46 @@ ...@@ -2,15 +2,46 @@
<div class="site-masthead"> <div class="site-masthead">
<div class="container"> <div class="container">
<nav class="nav"> <nav class="nav">
{% assign menu_items = site.pages | where:"menu",true | sort:"menu_order" %}
{% if menu_items.size > 1 %} {% for menu_index in (1..10) %}
{% for item in menu_items %} {% assign menu_items = site.pages | where:"menu",true | where: "menu_order",menu_index %}
{% if item.title %} {% if menu_items.size > 0 %}
<a class="nav-link {% if item.url == page.url %}active{% endif %}" href="{{ item.url | prepend: site.baseurl {% if menu_items.first.parent_menu %}
}}">{{ item.title }}</a> {% assign check_url = menu_items.first.parent_menu | downcase | prepend: '/' | append: '/' %}
{% endif %} <li class="dropdown">
<a class="nav-link {% if page.url contains check_url %}active{% endif %} dropbtn" href="#">{{ menu_items.first.parent_menu }}</a>
<div class="dropdown-content">
{% for item in menu_items %}
<a class="nav-link {% if item.url == page.url %}active{% endif %}" href="{{ item.url | prepend: site.baseurl }}">{{ item.title }}</a>
{% endfor %}
</div>
</li>
{% else %}
{% for item in menu_items %}
<li><a class="nav-link {% if item.url == page.url %}active{% endif %}" href="{{ item.url | prepend: site.baseurl }}">{{ item.title }}</a></li>
{% endfor %}
{% endif %}
{% endif %}
{% endfor %} {% endfor %}
{% endif %} <!--{% assign menu_items = site.pages | where:"menu",true | sort:"menu_order" %}-->
<!--{% if menu_items.size > 1 %}-->
<!--{% for item in menu_items %}-->
<!--{% if item.title %}-->
<!--{% if item.parent_menu %}-->
<!--<li class="dropdown">-->
<!--<a class="nav-link dropbtn" href="#">{{ item.parent_menu }}</a>-->
<!--{% assign sub_menu_items = site.pages | where:"menu",true | sort:"menu_order" %}-->
<!--<div class="dropdown-content">-->
<!--<a class="nav-link" href="#">aaaaaaaa</a>-->
<!--<a class="nav-link" href="#">bbbbbbbb</a>-->
<!--</div>-->
<!--</li>-->
<!--{% else %}-->
<!--<li><a class="nav-link {% if item.url contains page.url %}active{% endif %}" href="{{ item.url | prepend: site.baseurl }}">{{ item.title }}</a></li>-->
<!--{% endif %}-->
<!--{% endif %}-->
<!--{% endfor %}-->
<!--{% endif %}-->
</nav> </nav>
</div> </div>
</div> </div>
......
...@@ -7,10 +7,7 @@ layout: default ...@@ -7,10 +7,7 @@ layout: default
</div> </div>
{% assign research_pages = site.pages | where_exp: 'page', 'page.url contains "/research/"'%} {% assign research_pages = site.pages | where_exp: 'page', 'page.url contains "/research/"'%}
{% for item in research_pages reversed %} {% for item in research_pages reversed %}
{% if item.url contains "separationlogic" %}
{% else %}
<a class="btn btn-primary btn-lg" href="{{ item.url }}">{{ item.title }}</a> <a class="btn btn-primary btn-lg" href="{{ item.url }}">{{ item.title }}</a>
{% endif %}
{% endfor %} {% endfor %}
</div> </div>
......
...@@ -72,6 +72,24 @@ h6, .h6 { ...@@ -72,6 +72,24 @@ h6, .h6 {
*/ */
.site-masthead { .site-masthead {
li{
display:inline-block;
}
.dropdown-content {
display: none;
position: absolute;
background-color: $primary_colour;
min-width: 160px;
background-color: $primary_colour;
-webkit-box-shadow: inset 0 -.1rem .25rem rgba(0,0,0,.2);
box-shadow: inset 0 -.1rem .25rem rgba(0,0,0,.2);
}
.dropdown:hover .dropdown-content {
display: block;
}
margin-bottom: 3rem; margin-bottom: 3rem;
background-color: $primary_colour; background-color: $primary_colour;
-webkit-box-shadow: inset 0 -.1rem .25rem rgba(0,0,0,.2); -webkit-box-shadow: inset 0 -.1rem .25rem rgba(0,0,0,.2);
......
...@@ -2,7 +2,9 @@ ...@@ -2,7 +2,9 @@
title: Concurrency title: Concurrency
project_id: concurrency project_id: concurrency
menu: true menu: true
parent_menu: Research
menu_order: 3 menu_order: 3
sub_menu_order: 1
--- ---
We develop formal reasoning techniques for concurrent programs, with a We develop formal reasoning techniques for concurrent programs, with a
......
...@@ -2,7 +2,9 @@ ...@@ -2,7 +2,9 @@
title: JavaScript title: JavaScript
project_id: web project_id: web
menu: true menu: true
menu_order: 4 parent_menu: Research
menu_order: 3
sub_menu_order: 2
--- ---
We study the mechanised specification of the JavaScript language We study the mechanised specification of the JavaScript language
......
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
title: Separation Logic title: Separation Logic
project_id: sl project_id: sl
menu: true menu: true
parent_menu: Teaching
menu_order: 5 menu_order: 5
--- ---
...@@ -42,14 +43,14 @@ Feedback: Monday 21st of November ...@@ -42,14 +43,14 @@ Feedback: Monday 21st of November
Exam: 11th week Exam: 11th week
Recommended Reading: Mike Gordon has some excellent notes on [Hoare logic](http://www.cl.cam.ac.uk/~mjcg/Teaching/2011/Hoare/Notes/Notes.pdf), which briefly touches on separation logic in the last chapter. Recommended Reading: Mike Gordon has some [excellent notes on Hoare logic](http://www.cl.cam.ac.uk/~mjcg/Teaching/2011/Hoare/Notes/Notes.pdf), which briefly touches on separation logic in the last chapter.
Two good books on Hoare logic are: Logic in Computer Science: Modelling and Reasoning about Systems, Michael Huth and Mark Ryan, CUP, 2004; and The Formal Semantics of Programming Languages: an Introduction, Glynn Winskel, MIT Press, 1993. Two good books on Hoare logic are: Logic in Computer Science: Modelling and Reasoning about Systems, Michael Huth and Mark Ryan, CUP, 2004; and The Formal Semantics of Programming Languages: an Introduction, Glynn Winskel, MIT Press, 1993.
Most of the work on separation logic is in research papers. Most of the work on separation logic is in research papers.
Excellent introductions to separation logic include: O'Hearn, Reynolds and Yang's paper on [Local Reasoning about Programs that Alter Data Structures](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/localreasoning.pdf), CSL 2001, and John Reynolds' undergraduate course notes on separation logic and survey paper [Separation Logic: A Logic for Shared Mutable Data Structures](https://www.cs.cmu.edu/~jcr/seplogic.pdf), LICS 2002, both found on Reynolds' homepage. Excellent introductions to separation logic include: O'Hearn, Reynolds and Yang's paper on [Local Reasoning about Programs that Alter Data Structures](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/localreasoning.pdf), CSL 2001, and John Reynolds' undergraduate course notes on separation logic and survey paper [Separation Logic: A Logic for Shared Mutable Data Structures](https://www.cs.cmu.edu/~jcr/seplogic.pdf), LICS 2002, both found on Reynolds' homepage.
Andrew Appel has published a book on Program Logics for Certified Compilers, CUP 2014 (a copy is available in the [library](http://www.imperial.ac.uk/admin-services/library/)). Andrew Appel has published a book on Program Logics for Certified Compilers, CUP 2014 (a copy is available in the [library](http://www.imperial.ac.uk/admin-services/library/)).
Papers describing tool techniques include: [Symbolic Execution with Separation Logic](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.64.2006&rep=rep1&type=pdf), Berdine, Calcagno, O'Hearn, APLAS'05; [A Local Shape Analysis based on Separation Logic](http://www.eecs.qmul.ac.uk/~ddino/papers/localshape.pdf), Distefano, O'Hearn, Yang, TACAS 2006; and Compositional Shape Analysis by Means of Bi-abduction, Calcagno, Distefano, O'Hearn, Yang, JACM 2011. Papers describing tool techniques include: [Symbolic Execution with Separation Logic](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.64.2006&rep=rep1&type=pdf), Berdine, Calcagno, O'Hearn, APLAS'05; [A Local Shape Analysis based on Separation Logic](http://www.eecs.qmul.ac.uk/~ddino/papers/localshape.pdf), Distefano, O'Hearn, Yang, TACAS 2006; and [Compositional Shape Analysis by Means of Bi-abduction](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/jacm-abduction-webversion.pdf), Calcagno, Distefano, O'Hearn, Yang, JACM 2011.
The initial paper on concurrent separation logic is [Resources, Concurrency and Local Reasoning](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf), O'Hearn, TCS, 2007, and is worth a read. The initial paper on concurrent separation logic is [Resources, Concurrency and Local Reasoning](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf), O'Hearn, TCS, 2007, and is worth a read.
The survey paper [Steps in Modular Specifications of Concurrent Modules](https://www.doc.ic.ac.uk/~pg/papers/mfps15.pdf), da Rocha Pinto, Dinsdale-Young, Gardner, MFPS 2015, describes some modern developments in concurrent separation logics. The survey paper [Steps in Modular Specifications of Concurrent Modules](https://www.doc.ic.ac.uk/~pg/papers/mfps15.pdf), da Rocha Pinto, Dinsdale-Young, Gardner, MFPS 2015, describes some modern developments in concurrent separation logics.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment